![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantr1 | Structured version Visualization version GIF version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 27-Apr-2005.) |
Ref | Expression |
---|---|
3adantr.1 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Ref | Expression |
---|---|
3adantr1 | ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpc 1150 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 593 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: 3adant3r1 1182 3ad2antr3 1190 swopo 5554 omeulem1 8525 divmuldiv 11851 imasmnd2 18585 imasgrp2 18853 srgbinomlem2 19944 imasring 20030 abvdiv 20281 mdetunilem9 21953 lly1stc 22831 icccvx 24297 dchrpt 26599 dipsubdir 29676 poimirlem4 36049 fdc 36171 unichnidl 36457 dmncan1 36502 pexmidlem6N 38405 erngdvlem3 39420 erngdvlem3-rN 39428 dvalveclem 39455 dvhvaddass 39527 dvhlveclem 39538 issmflem 44900 prproropf1olem3 45629 |
Copyright terms: Public domain | W3C validator |