This rule is used to join two formulas using an AND connective, or when used backwards to split an AND formula into its two subformulas (to become seperate goals).
To use it forwards:

1. select an empty line and click on And Introduction.
2. then select, in the order you wish them to appear in the resulting formula, the two lines containing the formulas you require (Note these lines must be in the scope of the empty line).
3. the and formula will then be added to your proof.

1. select the conclusion or goal line in your proof or box (this line must be an AND formula) and click on And Introduction.
2. The two sub formulas will then appear as the conclusions in two new boxes (subproofs) in your proof.