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 11519 lediv23 11520 divalglem8 15739 isdrngd 19456 deg1tm 24639 ax5seglem1 26641 ax5seglem2 26642 nvaddsub4 28361 nmoub2i 28478 cdleme21at 37344 cdleme42f 37496 trlcoabs2N 37738 tendoplcl2 37794 tendopltp 37796 cdlemk2 37848 cdlemk8 37854 cdlemk9 37855 cdlemk9bN 37856 cdleml8 37999 dihglblem3N 38311 dihglblem3aN 38312 fourierdlem42 42311 lincscm 44413 itsclc0yqsol 44679 |
Copyright terms: Public domain | W3C validator |