![]() |
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 1141 | . 2 ⊢ ((𝜓 ∧ 𝜏 ∧ 𝜒) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 586 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: 3adant3r2 1191 po3nr 5290 funcnvqp 6200 sornom 9436 axdclem2 9679 fzadd2 12698 issubc3 16905 funcestrcsetclem9 17185 funcsetcestrclem9 17200 pgpfi 18415 imasring 19017 prdslmodd 19375 icoopnst 23157 iocopnst 23158 axcontlem4 26333 nvmdi 28092 mdsl3 29764 elicc3 32908 iscringd 34430 erngdvlem3 37153 erngdvlem3-rN 37161 dvalveclem 37188 dvhlveclem 37271 dvmptfprodlem 41101 smflimlem4 41923 funcringcsetcALTV2lem9 43073 funcringcsetclem9ALTV 43096 |
Copyright terms: Public domain | W3C validator |