| 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 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 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: 3adant3r2 1184 po3nr 5607 funcnvqp 6630 sornom 10317 axdclem2 10560 fzadd2 13599 issubc3 17894 funcestrcsetclem9 18193 funcsetcestrclem9 18208 pgpfi 19623 imasrng 20174 imasring 20327 prdslmodd 20967 icoopnst 24969 iocopnst 24970 axcontlem4 28982 nvmdi 30667 mdsl3 32335 elicc3 36318 iscringd 38005 erngdvlem3 40992 erngdvlem3-rN 41000 dvalveclem 41027 dvhlveclem 41110 dvmptfprodlem 45959 smflimlem4 46789 funcringcsetcALTV2lem9 48214 funcringcsetclem9ALTV 48237 |
| Copyright terms: Public domain | W3C validator |