**Description:** Introduce conjunct to both sides of an implication. (Contributed by NM, 3-Jan-1993)

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

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

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

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

1 | anim1i.1 | $${\u22a2}{\phi}\to {\psi}$$ | |

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

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