![]() |
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 1147 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 492 | 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: 3adant3r1 1198 3ad2antr3 1206 swopo 5195 omeulem1 7829 divmuldiv 10915 imasmnd2 17526 imasgrp2 17729 srgbinomlem2 18739 imasring 18817 abvdiv 19037 mdetunilem9 20626 lly1stc 21499 icccvx 22948 dchrpt 25189 dipsubdir 28010 poimirlem4 33724 fdc 33852 unichnidl 34141 dmncan1 34186 pexmidlem6N 35762 erngdvlem3 36778 erngdvlem3-rN 36786 dvalveclem 36814 dvhvaddass 36886 dvhlveclem 36897 issmflem 41440 |
Copyright terms: Public domain | W3C validator |