![]() |
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 476 | . 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓) | |
2 | ad4ant3.1 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) | |
3 | 1, 2 | syl3an2 1164 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: ltdiv23 11268 lediv23 11269 divalglem8 15530 isdrngd 19164 deg1tm 24315 ax5seglem1 26277 ax5seglem2 26278 nvaddsub4 28098 nmoub2i 28215 cdleme21at 36476 cdleme42f 36628 trlcoabs2N 36870 tendoplcl2 36926 tendopltp 36928 cdlemk2 36980 cdlemk8 36986 cdlemk9 36987 cdlemk9bN 36988 cdleml8 37131 dihglblem3N 37443 dihglblem3aN 37444 fourierdlem42 41285 lincscm 43226 itsclc0yqsol 43492 |
Copyright terms: Public domain | W3C validator |