![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adantl3 | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3adantl.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3adantl3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa 1004 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 3adantl.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan 474 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 189 df-an 373 df-3an 986 |
This theorem is referenced by: dif1en 7801 infpssrlem4 8733 fin23lem11 8744 tskwun 9206 gruf 9233 lediv2a 10497 prunioo 11758 rpnnen2lem7 14266 muldvds1 14320 muldvds2 14321 dvdscmul 14322 dvdsmulc 14323 rpexp 14665 pospropd 16373 mdetmul 19641 elcls 20082 iscnp4 20272 cnpnei 20273 cnpflf2 21008 cnpflf 21009 cnpfcf 21049 xbln0 21422 blcls 21514 iimulcl 21958 icccvx 21971 iscau2 22240 rrxcph 22344 cncombf 22607 mumul 24101 ax5seglem1 24951 ax5seglem2 24952 wwlkext2clwwlk 25524 nvmul0or 26266 fh1 27264 fh2 27265 cm2j 27266 pjoi0 27363 hoadddi 27449 hmopco 27669 padct 28300 iocinif 28356 volfiniune 29046 eulerpartlemb 29194 ivthALT 30984 cnambfre 31982 rngohomco 32206 rngoisoco 32214 pexmidlem3N 33531 hdmapglem7 35494 relexpmulg 36296 supxrgere 37550 supxrgelem 37554 supxrge 37555 lptre2pt 37714 dvnprodlem1 37815 ibliccsinexp 37821 iblioosinexp 37823 fourierdlem12 37975 fourierdlem41 38005 fourierdlem42 38006 fourierdlem42OLD 38007 fourierdlem48 38012 fourierdlem49 38013 fourierdlem51 38015 fourierdlem73 38037 fourierdlem74 38038 fourierdlem75 38039 fourierdlem97 38061 etransclem24 38117 sge0rpcpnf 38257 lincdifsn 40204 |
Copyright terms: Public domain | W3C validator |