![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > adantlrr | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.) |
Ref | Expression |
---|---|
adantl2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
adantlrr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl 459 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | adantl2.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylanl2 656 |
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 |
This theorem is referenced by: oelim 7233 odi 7277 marypha1lem 7944 dfac12lem2 8571 infunsdom 8641 isf34lem4 8804 distrlem1pr 9447 lcmgcdlem 14564 lcmdvds 14566 drsdirfi 16176 isacs3lem 16405 conjnmzb 16910 psgndif 19163 frlmsslsp 19347 metss2lem 21519 nghmcn 21759 bndth 21979 itg2monolem1 22701 dvmptfsum 22920 ply1divex 23080 itgulm 23356 rpvmasumlem 24318 dchrmusum2 24325 dchrisum0lem2 24349 dchrisum0lem3 24350 mulog2sumlem2 24366 pntibndlem3 24423 3v3e3cycl1 25365 4cycl4v4e 25387 blocni 26439 superpos 28000 chirredlem2 28037 eulerpartlemgvv 29202 ballotlemfc0 29318 ballotlemfcc 29319 bj-finsumval0 31695 fin2solem 31924 poimirlem28 31961 heicant 31968 ftc1anclem6 32015 ftc1anc 32018 fdc 32067 incsequz 32070 ismtyres 32133 isdrngo2 32190 rngohomco 32206 keridl 32258 linepsubN 33311 pmapsub 33327 mzpcompact2lem 35587 pellex 35673 monotuz 35783 unxpwdom3 35947 radcnvrat 36657 fprodexp 37668 fprodabs2 37669 dvnprodlem1 37815 stoweidlem34 37889 fourierdlem42 38006 fourierdlem42OLD 38007 elaa2 38093 sge0iunmptlemfi 38249 aacllem 40527 |
Copyright terms: Public domain | W3C validator |