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 1140 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜒)) | |
2 | 3adantr.1 | . 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) | |
3 | 1, 2 | sylan2 592 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: 3adant3r3 1176 3ad2antr1 1180 3ad2antr2 1181 sotr2 5498 dfwe2 7485 smogt 7993 infsupprpr 8956 wlogle 11161 fzadd2 12930 swrdspsleq 14015 tanadd 15508 prdsmndd 17932 mhmmnd 18159 imasring 19298 prdslmodd 19670 mpllsslem 20143 scmatlss 21062 mdetunilem3 21151 ptclsg 22151 tmdgsum2 22632 isxmet2d 22864 xmetres2 22898 prdsxmetlem 22905 comet 23050 iimulcl 23468 icoopnst 23470 iocopnst 23471 icccvx 23481 dvfsumrlim 24555 dvfsumrlim2 24556 colhp 26483 eengtrkg 26699 wwlksnredwwlkn 27600 dmdsl3 30019 eqgvscpbl 30846 resconn 32390 poimirlem28 34801 poimirlem32 34805 broucube 34807 ftc1anclem7 34854 ftc1anc 34856 isdrngo2 35117 iscringd 35157 unichnidl 35190 lplnle 36556 2llnjN 36583 2lplnj 36636 osumcllem11N 36982 cdleme1 37243 erngplus2 37820 erngplus2-rN 37828 erngdvlem3 38006 erngdvlem3-rN 38014 dvaplusgv 38026 dvalveclem 38041 dvhvaddass 38113 dvhlveclem 38124 dihmeetlem12N 38334 issmflem 42881 fmtnoprmfac1 43604 lincresunit3lem2 44463 lincresunit3 44464 |
Copyright terms: Public domain | W3C validator |