| 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 395 ∧ w3a 1086 |
| 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 207 df-an 396 df-3an 1088 |
| This theorem is referenced by: 3adant3r1 1183 3ad2antr3 1191 swopo 5543 omeulem1 8509 divmuldiv 11841 imasmnd2 18699 imasgrp2 18985 imasrng 20112 srgbinomlem2 20162 imasring 20266 abvdiv 20762 mdetunilem9 22564 lly1stc 23440 icccvx 24904 dchrpt 27234 dipsubdir 30923 poimirlem4 37825 fdc 37946 unichnidl 38232 dmncan1 38277 pexmidlem6N 40235 erngdvlem3 41250 erngdvlem3-rN 41258 dvalveclem 41285 dvhvaddass 41357 dvhlveclem 41368 issmflem 46971 prproropf1olem3 47751 |
| Copyright terms: Public domain | W3C validator |