![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantr2 | 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 |
---|---|
3adantr2 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpb 1146 | . 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 591 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: 3adant3r2 1180 po3nr 5605 funcnvqp 6618 sornom 10307 axdclem2 10550 fzadd2 13576 issubc3 17843 funcestrcsetclem9 18147 funcsetcestrclem9 18162 pgpfi 19577 imasrng 20134 imasring 20283 prdslmodd 20870 icoopnst 24912 iocopnst 24913 axcontlem4 28855 nvmdi 30535 mdsl3 32203 elicc3 35934 iscringd 37604 erngdvlem3 40595 erngdvlem3-rN 40603 dvalveclem 40630 dvhlveclem 40713 dvmptfprodlem 45472 smflimlem4 46302 funcringcsetcALTV2lem9 47548 funcringcsetclem9ALTV 47571 |
Copyright terms: Public domain | W3C validator |