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  2626  2mo  2648  mosubopt  5448  predpoirr  6266  predfrirr  6267  funfv  6905  dffv2  6913  fvmptnf  6947  rdgsucmptnf  8322  frsucmptn  8332  mapdom2  9005  frfi  9145  oiexg  9384  wemapwe  9546  r1tr  9625  alephsing  10125  uzin  12711  fundmge2nop0  14298  fun2dmnop0  14300  wrdnfi  14343  relexpsucrd  14835  relexpsucld  14836  relexpreld  14842  relexpdmd  14846  relexprnd  14850  relexpfldd  14852  relexpaddd  14856  dfrtrclrec2  14860  rtrclreclem4  14863  dfrtrcl2  14864  relexpindlem  14865  sumrblem  15514  fsumcvg  15515  summolem2a  15518  fsumcvg2  15530  prodeq2ii  15714  prodrblem  15730  fprodcvg  15731  prodmolem2a  15735  zprod  15738  ptpjpre1  22820  qtopres  22947  fgabs  23128  ptcmplem3  23303  setsmstopn  23731  tngtopn  23912  cnmpopc  24189  pcoval2  24277  pcopt  24283  pcopt2  24284  itgle  25072  ibladdlem  25082  iblabslem  25090  iblabs  25091  iblabsr  25092  iblmulc2  25093  bddiblnc  25104  ditgneg  25119  logbgcd1irr  26042  umgr2adedgspth  28514  n4cyclfrgr  28856  poimirlem26  35901  poimirlem32  35907  ovoliunnfl  35917  voliunnfl  35919  volsupnfl  35920  itg2addnclem  35926  itg2gt0cn  35930  ibladdnclem  35931  iblabsnclem  35938  iblabsnc  35939  iblmulc2nc  35940  ftc1anclem7  35954  ftc1anclem8  35955  ftc1anc  35956  dicvalrelN  39446  dihvalrel  39540  ldepspr  46154  naryfval  46314  naryfvalixp  46315