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 1053 | . 2 ⊢ ((𝜏 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 490 | 1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3ad2antr3 1221 3adant3r1 1266 swopo 4969 omeulem1 7549 divmuldiv 10604 imasmnd2 17150 imasgrp2 17353 srgbinomlem2 18364 imasring 18442 abvdiv 18660 mdetunilem9 20245 lly1stc 21109 icccvx 22557 dchrpt 24792 dipsubdir 27087 poimirlem4 32583 fdc 32711 unichnidl 33000 dmncan1 33045 pexmidlem6N 34279 erngdvlem3 35296 erngdvlem3-rN 35304 dvalveclem 35332 dvhvaddass 35404 dvhlveclem 35415 issmflem 39613 |
Copyright terms: Public domain | W3C validator |