**Description:** Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995)

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

Hypothesis | 3adant.1 | $${\u22a2}\left({\phi}\wedge {\psi}\right)\to {\chi}$$ | |

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

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

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

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

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