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 1060 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 491 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 |
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 386 df-3an 1039 |
This theorem is referenced by: 3ad2antr3 1228 3adant3r1 1274 swopo 5045 omeulem1 7662 divmuldiv 10725 imasmnd2 17327 imasgrp2 17530 srgbinomlem2 18541 imasring 18619 abvdiv 18837 mdetunilem9 20426 lly1stc 21299 icccvx 22749 dchrpt 24992 dipsubdir 27703 poimirlem4 33413 fdc 33541 unichnidl 33830 dmncan1 33875 pexmidlem6N 35261 erngdvlem3 36278 erngdvlem3-rN 36286 dvalveclem 36314 dvhvaddass 36386 dvhlveclem 36397 issmflem 40936 |
Copyright terms: Public domain | W3C validator |