![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantr3 | 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 |
---|---|
3adantr3 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 1078 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 490 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
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 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3ad2antr1 1246 3ad2antr2 1247 3adant3r3 1297 sotr2 5093 dfwe2 7023 smogt 7509 wlogle 10599 fzadd2 12414 tanadd 14941 prdsmndd 17370 mhmmnd 17584 imasring 18665 prdslmodd 19017 mpllsslem 19483 scmatlss 20379 mdetunilem3 20468 ptclsg 21466 tmdgsum2 21947 isxmet2d 22179 xmetres2 22213 prdsxmetlem 22220 comet 22365 iimulcl 22783 icoopnst 22785 iocopnst 22786 icccvx 22796 dvfsumrlim 23839 dvfsumrlim2 23840 colhp 25707 eengtrkg 25910 wwlksnredwwlkn 26858 dmdsl3 29302 resconn 31354 poimirlem28 33567 poimirlem32 33571 broucube 33573 ftc1anclem7 33621 ftc1anc 33623 isdrngo2 33887 iscringd 33927 unichnidl 33960 lplnle 35144 2llnjN 35171 2lplnj 35224 osumcllem11N 35570 cdleme1 35832 erngplus2 36409 erngplus2-rN 36417 erngdvlem3 36595 erngdvlem3-rN 36603 dvaplusgv 36615 dvalveclem 36631 dvhvaddass 36703 dvhlveclem 36714 dihmeetlem12N 36924 issmflem 41257 fmtnoprmfac1 41802 lincresunit3lem2 42594 lincresunit3 42595 |
Copyright terms: Public domain | W3C validator |