Theorem pm2.61i 110

Description: Inference eliminating an antecedent.

Hypotheses

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

Assertion

Ref	Expression
pm2.61i	⊢ ψ

Proof of Theorem pm2.61i

Step	Hyp	Ref	Expression
1		pm2.61i.1	. 2 ⊢ (φ → ψ)
2		pm2.61i.2	. 2 ⊢ (¬ φ → ψ)
3		pm2.61 109	. 2 ⊢ ((φ → ψ) → ((¬ φ → ψ) → ψ))
4	1, 2, 3	mp2 43	1 ⊢ ψ

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  pm2.61d2 111  pm2.61d 112  pm2.61ii 113  pm2.61iii 114  ja 118  pm2.61an1 364  pm5.21nii 504  4cases 565  elimh 571  consensus 574  eqid 810  eqvin.l1 851  sb6y 872  hbsb3 875  sbn1 880  sbi1 884  hbsb4 905  ddelimf2 907  sbidm 912  sbco2 913  sbco3 915  sbcom 916  sb9i 920  ax11a 926  hbs1 986  hbsb 987  sbal1 996  sbal 997  hbeu 1016  mo 1020  moexex 1058  hbab 1096  rgen2 1248  ralcom2 1314  alexeq 1409  eueq2 1429  moeq3 1432  mo2icl 1434  sbc2or 1454  unineq 1680  noel 1711  class2set 1747  ralidm 1774  raaan 1775  elimhyp 1790  elimhyp2v 1791  elimhyp3v 1792  keephyp 1794  keephyp3v 1795  snsspr 1853  snex 1859  dtru 1889  prex 1892  opth2 1909  mosubop 1911  onfr 2237  nsuceq0 2306  trsuc 2308  ordsuc 2318  ordsucelsuc 2324  nlimsuc 2363  vtoclrbr 2450  vtoclibr 2451  relsn 2485  opeldm 2534  dmsnop 2547  dmxpid 2553  soirri 2629  fconst 2774  tz6.12-2 2845  ndmfv 2848  fveqres 2851  fvopabn 2873  cleqfv 2880  fvelrn 2883  fconstfv 2903  rdgsucopabn 2985  ndmoprcl 3058  ndmord 3064  1stval 3089  2ndval 3090  1st2val 3097  om0x 3126  breng 3280  brdomg 3281  sdomirr 3314  snfi 3337  unen 3338  pw2en 3348  ensdomtr 3372  sdomen2 3380  en2lp 3453  r1tr 3498  rankon 3515  r1pw 3529  r1pwcl 3530  scottex 3541  numth2 3600  fodomb 3615  cardval 3633  cardcard 3655  alephon 3671  alephcard 3673  alephnbtwn 3674  alephnbtwn2 3675  alephsucdom 3685  cfub 3703  cardcf 3706  cflecard 3707  cfle 3708  axunndlem1 3741  axpownd 3747  addcompi 3816  addasspi 3817  mulcompi 3818  mulasspi 3819  distrpi 3820  addnidpi 3822  nlt1pi 3827  addcompq 3856  addasspq 3857  mulcompq 3858  mulasspq 3859  distrpq 3861  genpass 3906  addcompr 3917  mulcompr 3919  distrpr 3926  ltexprlem7 3942  addcomsr 3990  addasssr 3991  mulcomsr 3992  mulasssr 3993  distrsr 3994  sqge0 4344  nnwoOLD 4608  ruclem13 4897  ruclem24 4908  ruclem26 4910  ruclem27 4911  ruclem28 4912  bcs 5101  occllem7 5186  h1de2ctlem 5460  mdsym 5784

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

metamath.org