Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant2r | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.) |
Ref | Expression |
---|---|
ad4ant3.1 | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
3adant2r | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 483 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an2 1156 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 df-3an 1081 |
This theorem is referenced by: ltdiv23 11520 lediv23 11521 divalglem8 15741 isdrngd 19458 deg1tm 24641 ax5seglem1 26642 ax5seglem2 26643 nvaddsub4 28362 nmoub2i 28479 cdleme21at 37346 cdleme42f 37498 trlcoabs2N 37740 tendoplcl2 37796 tendopltp 37798 cdlemk2 37850 cdlemk8 37856 cdlemk9 37857 cdlemk9bN 37858 cdleml8 38001 dihglblem3N 38313 dihglblem3aN 38314 fourierdlem42 42315 lincscm 44383 itsclc0yqsol 44649 |
Copyright terms: Public domain | W3C validator |