| 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 1151 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
| 2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
| 3 | 1, 2 | sylan2 593 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1087 |
| 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 1089 |
| This theorem is referenced by: 3adant3r1 1183 3ad2antr3 1191 swopo 5603 omeulem1 8620 divmuldiv 11967 imasmnd2 18787 imasgrp2 19073 imasrng 20174 srgbinomlem2 20224 imasring 20327 abvdiv 20830 mdetunilem9 22626 lly1stc 23504 icccvx 24981 dchrpt 27311 dipsubdir 30867 poimirlem4 37631 fdc 37752 unichnidl 38038 dmncan1 38083 pexmidlem6N 39977 erngdvlem3 40992 erngdvlem3-rN 41000 dvalveclem 41027 dvhvaddass 41099 dvhlveclem 41110 issmflem 46742 prproropf1olem3 47492 |
| Copyright terms: Public domain | W3C validator |