Theorem pm2.61i 156

Description: Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses

Ref	Expression
pm2.61i.1	⊢ (φ → ψ)
pm2.61i.2	⊢ (¬ φ → ψ)

Assertion

Ref	Expression
pm2.61i	⊢ ψ

Proof of Theorem 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 5	1 ⊢ ψ

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:  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  2592  pm2.61ine  2593  rgen2a  2681  ralcom2  2776  eueq2  3011  moeq3  3014  mo2icl  3016  sbc2or  3055  unineq  3506  ralidm  3654  ifsb  3672  ifid  3695  ifnot  3701  ifan  3702  ifor  3703  elimhyp  3711  elimhyp2v  3712  elimhyp3v  3713  elimhyp4v  3714  elimdhyp  3716  keephyp2v  3718  keephyp3v  3719  ssunsn2  3866  snex  4112  setswith  4322  iotassuni  4356  iotaex  4357  dfiota3  4371  dfiota4  4373  snfi  4432  eqtfinrelk  4487  dfphi2  4570  copsexg  4608  phiall  4619  dfid3  4769  imasn  5019  dmsnopss  5068  fveqres  5356  eqfnfv  5393  f0cli  5419  fvunsn  5445  fconst5  5456  elimdelov  5574  ndmovcl  5615  ndmovord  5621  fvmptss  5706  fvmptex  5722  fvmptss2  5726  fvfullfun  5865  nchoicelem12  6301  frecxp  6315