| 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 1163 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
| 2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylan2 602 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 399 ∧ w3a 1098 |
| 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 209 df-an 400 df-3an 1100 |
| This theorem is referenced by: 3adant3r1 1196 3ad2antr3 1204 swopo 5566 omeulem1 8551 divmuldiv 11891 imasmnd2 18808 imasgrp2 19097 imasrng 20223 srgbinomlem2 20273 imasring 20375 abvdiv 20875 mdetunilem9 22677 lly1stc 23553 icccvx 25009 dchrpt 27328 dipsubdir 31048 poimirlem4 38120 fdc 38241 unichnidl 38527 dmncan1 38572 pexmidlem6N 40596 erngdvlem3 41611 erngdvlem3-rN 41619 dvalveclem 41646 dvhvaddass 41718 dvhlveclem 41729 issmflem 47298 prproropf1olem3 48108 |
| Copyright terms: Public domain | W3C validator |