| 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 20277 imasring 20379 abvdiv 20878 mdetunilem9 22680 lly1stc 23556 icccvx 25012 dchrpt 27331 dipsubdir 31051 poimirlem4 38123 fdc 38244 unichnidl 38530 dmncan1 38575 pexmidlem6N 40599 erngdvlem3 41614 erngdvlem3-rN 41622 dvalveclem 41649 dvhvaddass 41721 dvhlveclem 41732 issmflem 47301 prproropf1olem3 48111 |
| Copyright terms: Public domain | W3C validator |