Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adantr3 | Structured version Visualization version Unicode 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 1058 | . 2 | |
2 | 3adantr.1 | . 2 | |
3 | 1, 2 | sylan2 491 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 386 df-3an 1039 |
This theorem is referenced by: 3ad2antr1 1226 3ad2antr2 1227 3adant3r3 1276 sotr2 5064 dfwe2 6981 smogt 7464 wlogle 10561 fzadd2 12376 tanadd 14897 prdsmndd 17323 mhmmnd 17537 imasring 18619 prdslmodd 18969 mpllsslem 19435 scmatlss 20331 mdetunilem3 20420 ptclsg 21418 tmdgsum2 21900 isxmet2d 22132 xmetres2 22166 prdsxmetlem 22173 comet 22318 iimulcl 22736 icoopnst 22738 iocopnst 22739 icccvx 22749 dvfsumrlim 23794 dvfsumrlim2 23795 colhp 25662 eengtrkg 25865 wwlksnredwwlkn 26790 dmdsl3 29174 resconn 31228 poimirlem28 33437 poimirlem32 33441 broucube 33443 ftc1anclem7 33491 ftc1anc 33493 isdrngo2 33757 iscringd 33797 unichnidl 33830 lplnle 34826 2llnjN 34853 2lplnj 34906 osumcllem11N 35252 cdleme1 35514 erngplus2 36092 erngplus2-rN 36100 erngdvlem3 36278 erngdvlem3-rN 36286 dvaplusgv 36298 dvalveclem 36314 dvhvaddass 36386 dvhlveclem 36397 dihmeetlem12N 36607 issmflem 40936 fmtnoprmfac1 41477 lincresunit3lem2 42269 lincresunit3 42270 |
Copyright terms: Public domain | W3C validator |