Theorem pm2.61d1 180

Description: Inference eliminating an antecedent. (Contributed by NM, 15-Jul-2005.)

Hypotheses

Ref	Expression
pm2.61d1.1	⊢ (𝜑 → (𝜓 → 𝜒))
pm2.61d1.2	⊢ (¬ 𝜓 → 𝜒)

Assertion

Ref	Expression
pm2.61d1	⊢ (𝜑 → 𝜒)

Proof of Theorem 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 179	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.61nii  184  ja  186  pm2.01d  189  moexexlem  2622  2mo  2644  mosubopt  5510  predpoirr  6334  predfrirr  6335  funfv  6978  dffv2  6986  fvmptnf  7020  rdgsucmptnf  8431  frsucmptn  8441  mapdom2  9150  frfi  9290  oiexg  9532  wemapwe  9694  r1tr  9773  alephsing  10273  uzin  12864  fundmge2nop0  14455  fun2dmnop0  14457  wrdnfi  14500  relexpsucrd  14982  relexpsucld  14983  relexpreld  14989  relexpdmd  14993  relexprnd  14997  relexpfldd  14999  relexpaddd  15003  dfrtrclrec2  15007  rtrclreclem4  15010  dfrtrcl2  15011  relexpindlem  15012  sumrblem  15659  fsumcvg  15660  summolem2a  15663  fsumcvg2  15675  prodeq2ii  15859  prodrblem  15875  fprodcvg  15876  prodmolem2a  15880  zprod  15883  ptpjpre1  23082  qtopres  23209  fgabs  23390  ptcmplem3  23565  setsmstopn  23993  tngtopn  24174  cnmpopc  24451  pcoval2  24539  pcopt  24545  pcopt2  24546  itgle  25334  ibladdlem  25344  iblabslem  25352  iblabs  25353  iblabsr  25354  iblmulc2  25355  bddiblnc  25366  ditgneg  25381  logbgcd1irr  26306  umgr2adedgspth  29240  n4cyclfrgr  29582  poimirlem26  36600  poimirlem32  36606  ovoliunnfl  36616  voliunnfl  36618  volsupnfl  36619  itg2addnclem  36625  itg2gt0cn  36629  ibladdnclem  36630  iblabsnclem  36637  iblabsnc  36638  iblmulc2nc  36639  ftc1anclem7  36653  ftc1anclem8  36654  ftc1anc  36655  dicvalrelN  40142  dihvalrel  40236  ldepspr  47232  naryfval  47392  naryfvalixp  47393