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  2629  2mo  2651  mosubopt  5425  predpoirr  6240  predfrirr  6241  funfv  6864  dffv2  6872  fvmptnf  6906  rdgsucmptnf  8269  frsucmptn  8279  mapdom2  8944  frfi  9068  oiexg  9303  wemapwe  9464  r1tr  9543  alephsing  10041  uzin  12627  fundmge2nop0  14215  fun2dmnop0  14217  wrdnfi  14260  relexpsucrd  14753  relexpsucld  14754  relexpreld  14760  relexpdmd  14764  relexprnd  14768  relexpfldd  14770  relexpaddd  14774  dfrtrclrec2  14778  rtrclreclem4  14781  dfrtrcl2  14782  relexpindlem  14783  sumrblem  15432  fsumcvg  15433  summolem2a  15436  fsumcvg2  15448  prodeq2ii  15632  prodrblem  15648  fprodcvg  15649  prodmolem2a  15653  zprod  15656  ptpjpre1  22731  qtopres  22858  fgabs  23039  ptcmplem3  23214  setsmstopn  23642  tngtopn  23823  cnmpopc  24100  pcoval2  24188  pcopt  24194  pcopt2  24195  itgle  24983  ibladdlem  24993  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  bddiblnc  25015  ditgneg  25030  logbgcd1irr  25953  umgr2adedgspth  28322  n4cyclfrgr  28664  poimirlem26  35812  poimirlem32  35818  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnclem  35837  itg2gt0cn  35841  ibladdnclem  35842  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  dicvalrelN  39206  dihvalrel  39300  ldepspr  45825  naryfval  45985  naryfvalixp  45986