![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61d1 | Structured version Visualization version GIF 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 172 | 1 ⊢ (𝜑 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem is referenced by: ja 175 pm2.61nii 179 pm2.01d 182 moexexvw 2661 2moswapv 2662 moexex 2669 2mo 2679 mosubopt 5256 predpoirr 6014 predfrirr 6015 funfv 6578 dffv2 6584 fvmptnf 6616 rdgsucmptnf 7869 frsucmptn 7878 mapdom2 8484 frfi 8558 oiexg 8794 wemapwe 8954 r1tr 8999 alephsing 9496 uzin 12092 fundmge2nop0 13661 fun2dmnop0 13663 wrdnfi 13710 sumrblem 14928 fsumcvg 14929 summolem2a 14932 fsumcvg2 14944 prodeq2ii 15127 prodrblem 15143 fprodcvg 15144 prodmolem2a 15148 zprod 15151 ptpjpre1 21883 qtopres 22010 fgabs 22191 ptcmplem3 22366 setsmstopn 22791 tngtopn 22962 cnmpopc 23235 pcoval2 23323 pcopt 23329 pcopt2 23330 itgle 24113 ibladdlem 24123 iblabslem 24131 iblabs 24132 iblabsr 24133 iblmulc2 24134 ditgneg 24158 logbgcd1irr 25073 umgr2adedgspth 27454 n4cyclfrgr 27825 poimirlem26 34365 poimirlem32 34371 ovoliunnfl 34381 voliunnfl 34383 volsupnfl 34384 itg2addnclem 34390 itg2gt0cn 34394 ibladdnclem 34395 iblabsnclem 34402 iblabsnc 34403 iblmulc2nc 34404 bddiblnc 34409 ftc1anclem7 34420 ftc1anclem8 34421 ftc1anc 34422 dicvalrelN 37772 dihvalrel 37866 ldepspr 43901 |
Copyright terms: Public domain | W3C validator |