New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > pm2.61i | GIF version |
Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.) |
Ref | Expression |
---|---|
pm2.61i.1 | ⊢ (φ → ψ) |
pm2.61i.2 | ⊢ (¬ φ → ψ) |
Ref | Expression |
---|---|
pm2.61i | ⊢ ψ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (φ → φ) | |
2 | pm2.61i.2 | . . 3 ⊢ (¬ φ → ψ) | |
3 | pm2.61i.1 | . . 3 ⊢ (φ → ψ) | |
4 | 2, 3 | ja 153 | . 2 ⊢ ((φ → φ) → ψ) |
5 | 1, 4 | ax-mp 8 | 1 ⊢ ψ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem is referenced by: pm2.61ii 157 pm2.61nii 158 pm2.61iii 159 pm2.65i 165 pm5.21nii 342 pm5.18 345 biass 348 pm2.61ian 765 ecase3 907 4cases 915 elimh 922 pm4.42 926 3ecase 1286 ax9 1949 dvelimh 1964 exdistrf 1971 equveli 1988 dfsb2 2055 sbn 2062 sbi1 2063 sbco2 2086 sbco3 2088 sb9i 2094 ax11v 2096 hbs1 2105 nfsb 2109 sbal1 2126 sbal 2127 dvelimALT 2133 ax11 2155 equid1 2158 equid1ALT 2176 dvelimf-o 2180 ax11inda2ALT 2198 ax11inda2 2199 eujustALT 2207 moexex 2273 pm2.61ne 2591 pm2.61ine 2592 rgen2a 2680 ralcom2 2775 eueq2 3010 moeq3 3013 mo2icl 3015 sbc2or 3054 unineq 3505 ralidm 3653 ifsb 3671 ifid 3694 ifnot 3700 ifan 3701 ifor 3702 elimhyp 3710 elimhyp2v 3711 elimhyp3v 3712 elimhyp4v 3713 elimdhyp 3715 keephyp2v 3717 keephyp3v 3718 ssunsn2 3865 snex 4111 setswith 4321 iotassuni 4355 iotaex 4356 dfiota3 4370 dfiota4 4372 snfi 4431 eqtfinrelk 4486 dfphi2 4569 copsexg 4607 phiall 4618 dfid3 4768 imasn 5018 dmsnopss 5067 fveqres 5355 eqfnfv 5392 f0cli 5418 fvunsn 5444 fconst5 5455 elimdelov 5573 ndmovcl 5614 ndmovord 5620 fvmptss 5705 fvmptex 5721 fvmptss2 5725 fvfullfun 5864 nchoicelem12 6300 frecxp 6314 |
Copyright terms: Public domain | W3C validator |