Theorem pm2.61i 126

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 124	. 2 ⊢ ((φ → ψ) → ((¬ φ → ψ) → ψ))
4	1, 2, 3	mp2 43	1 ⊢ ψ

Syntax hints:  ¬ wn 2   → wi 3

This theorem is referenced by:  pm2.61d 127  pm2.61ii 130  pm2.61nii 131  pm2.61iii 132  pm2.61ian 475  pm5.21nii 676  biass 741  4cases 755  elimh 761  consensus 764  pm4.42 765  3ecase 919  equid 1113  dvelimfALT 1136  equvini 1151  ax11 1203  dfsb2 1209  sbn 1215  sbi1 1216  hbsb4 1232  sbidm 1238  sbco2 1239  sbco3 1241  sb9i 1247  ax11v 1249  hbs1 1314  hbsb 1315  sbal1 1328  sbal 1329  ax11inda2ALT 1346  ax11inda2 1347  a12lem1 1353  hbeu 1366  mo 1370  moexex 1415  2mo 1424  hbab 1444  pm2.61ine 1610  rgen2a 1675  ralcom2 1752  eueq2 1890  moeq3 1893  mo2icl 1895  sbc2or 1929  unineq 2226  noel 2255  ralidm 2328  ifid 2347  ifswap 2353  elimhyp 2361  elimhyp2v 2362  elimhyp3v 2363  elimhyp4v 2364  elimdhyp 2366  keephyp2v 2368  keephyp3v 2369  snsspr 2440  intabs 2701  class2set 2702  dtruALT 2716  snex 2718  dtru 2740  opth2 2765  dfid3 2799  unisn2 2839  nsuceq0 3016  trsuc 3018  ordsuc 3028  ordsucelsuc 3036  vtoclrbr 3174  vtoclibr 3175  relsn 3216  opeldm 3271  dmsnop 3285  soirri 3391  tz6.12-2 3678  ndmfv 3684  fveqres 3688  fvopabn 3725  eqfnfv 3736  fconst5 3787  rdgsucopabn 3886  elimdeloprv 3940  ndmoprcl 3984  ndmord 3990  1stval 4019  2ndval 4020  1st2val 4033  2nd2val 4034  om0x 4096  breng 4311  brdomg 4312  snfi 4367  unen 4368  pw2en 4380  ensdomtr 4405  sdomirr 4406  sdomen2 4416  en2lp 4526  r1tr 4578  rankon 4595  r1pw 4610  r1pwcl 4611  rankuni 4622  scottex 4640  numth2 4709  cardval 4750  cardidm 4772  alephon 4788  alephcard 4790  alephnbtwn 4791  alephnbtwn2 4792  alephsucdom 4803  cfub 4831  cardcf 4834  cflecard 4835  cfle 4836  axunndlem1 4870  axpownd 4876  addcompi 4945  addasspi 4946  mulcompi 4947  mulasspi 4948  distrpi 4949  addnidpi 4951  nlt1pi 4956  addcompq 4985  addasspq 4986  mulcompq 4987  mulasspq 4988  distrpq 4990  genpass 5035  addcompr 5046  mulcompr 5048  distrpr 5055  ltexprlem7 5071  addcomsr 5119  addasssr 5120  mulcomsr 5121  mulasssr 5122  distrsr 5123  ndmioo 6258  iooid 6259  ioossre 6279  uzssz 6313  uzwo 6338  uzwoOLD 6339  elfzlem 6356  clmi1 6975  isumshft 7090  isumshft2 7091  ruclem13 7416  ruclem24 7427  ruclem26 7429  ruclem27 7430  ruclem28 7431  iooretop 7552  dscmet 7804  vafval 8102  bafval 8103  smfval 8104  0vfval 8105  vsfval 8132  elioo1t3 8740  oisbmi 8741  oisbmj 8742  hmeogrp 8776  cnfilca 8801  domval 8849  codval 8850  idval 8851  cmpval 8852  avril1 8964  bcsALT 9195  h1de2ctlem 9608  lnopcon 10092  lnfncon 10119

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

Copyright terms: Public domain