![]() |
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 474 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an2 1168 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 |
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 197 df-an 385 df-3an 1074 |
This theorem is referenced by: ltdiv23 11102 lediv23 11103 divalglem8 15321 isdrngd 18970 deg1tm 24073 ax5seglem1 26003 ax5seglem2 26004 nvaddsub4 27817 nmoub2i 27934 cdleme21at 36114 cdleme42f 36266 trlcoabs2N 36508 tendoplcl2 36564 tendopltp 36566 cdlemk2 36618 cdlemk8 36624 cdlemk9 36625 cdlemk9bN 36626 cdleml8 36769 dihglblem3N 37082 dihglblem3aN 37083 fourierdlem42 40865 lincscm 42725 |
Copyright terms: Public domain | W3C validator |