# Conjunction introduction

Transformation rules |
---|

Propositional calculus |

Rules of inference |

Rules of replacement |

Predicate logic |

**Conjunction introduction** (often abbreviated simply as **conjunction** and also called **and introduction**^{[1]}^{[2]}^{[3]}) is a valid rule of inference of propositional logic. The rule makes it possible to introduce a conjunction into a logical proof. It is the inference that if the proposition *p* is true, and proposition *q* is true, then the logical conjunction of the two propositions *p and q* is true. For example, if it's true that it's coming, and it's true that I'm inside, then it's true that "it's coming and I'm inside". The rule can be stated:

where the rule is that wherever an instance of "" and "" appear on lines of a proof, a "" can be placed on a subsequent line.

## Formal notation

The *conjunction introduction* rule may be written in sequent notation:

where is a metalogical symbol meaning that is a syntactic consequence if and are each on lines of a proof in some logical system;

where and are propositions expressed in some formal system.