![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61d1 | Structured version Visualization version Unicode version |
Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.) |
Ref | Expression |
---|---|
pm2.61d1.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm2.61d1.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.61d1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61d1.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm2.61d1.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | a1i 11 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | pm2.61d 163 |
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 is referenced by: ja 166 pm2.61nii 171 pm2.01d 174 moexex 2380 2mo 2390 mosubopt 4712 predpoirr 5426 predfrirr 5427 funfv 5954 dffv2 5960 fvmptnf 5989 rdgsucmptnf 7172 frsucmptn 7181 mapdom2 7768 frfi 7841 oiexg 8075 wemapwe 8227 r1tr 8272 alephsing 8731 uzin 11219 sumrblem 13825 fsumcvg 13826 summolem2a 13829 fsumcvg2 13841 prodeq2ii 14015 prodrblem 14031 fprodcvg 14032 prodmolem2a 14036 zprod 14039 ptpjpre1 20634 qtopres 20761 fgabs 20942 ptcmplem3 21117 setsmstopn 21541 tngtopn 21706 cnmpt2pc 22004 pcoval2 22095 pcopt 22101 pcopt2 22102 itgle 22815 ibladdlem 22825 iblabslem 22833 iblabs 22834 iblabsr 22835 iblmulc2 22836 ditgneg 22860 nbgra0nb 25205 n4cyclfrgra 25794 poimirlem26 32010 poimirlem32 32016 ovoliunnfl 32026 voliunnfl 32028 volsupnfl 32029 itg2addnclem 32037 itg2gt0cn 32041 ibladdnclem 32042 iblabsnclem 32049 iblabsnc 32050 iblmulc2nc 32051 bddiblnc 32056 ftc1anclem7 32067 ftc1anclem8 32068 ftc1anc 32069 dicvalrelN 34797 dihvalrel 34891 fundmge2nop 39067 fun2dmnop 39068 umgr2adedgspth 39896 ldepspr 40538 |
Copyright terms: Public domain | W3C validator |