**Description:** Add two conjuncts to antecedent and consequent. (Contributed by Jeff
Hankins, 16-Aug-2009)

Ref | Expression | ||
---|---|---|---|

Hypothesis | 3animi.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

Assertion | 3anim1i | $${\u22a2}\left({\phi}\wedge {\chi}\wedge {\theta}\right)\to \left({\psi}\wedge {\chi}\wedge {\theta}\right)$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 3animi.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

2 | id | $${\u22a2}{\chi}\to {\chi}$$ | |

3 | id | $${\u22a2}{\theta}\to {\theta}$$ | |

4 | 1 2 3 | 3anim123i | $${\u22a2}\left({\phi}\wedge {\chi}\wedge {\theta}\right)\to \left({\psi}\wedge {\chi}\wedge {\theta}\right)$$ |