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  2623  2mo  2645  mosubopt  5511  predpoirr  6335  predfrirr  6336  funfv  6979  dffv2  6987  fvmptnf  7021  rdgsucmptnf  8429  frsucmptn  8439  mapdom2  9148  frfi  9288  oiexg  9530  wemapwe  9692  r1tr  9771  alephsing  10271  uzin  12862  fundmge2nop0  14453  fun2dmnop0  14455  wrdnfi  14498  relexpsucrd  14980  relexpsucld  14981  relexpreld  14987  relexpdmd  14991  relexprnd  14995  relexpfldd  14997  relexpaddd  15001  dfrtrclrec2  15005  rtrclreclem4  15008  dfrtrcl2  15009  relexpindlem  15010  sumrblem  15657  fsumcvg  15658  summolem2a  15661  fsumcvg2  15673  prodeq2ii  15857  prodrblem  15873  fprodcvg  15874  prodmolem2a  15878  zprod  15881  ptpjpre1  23075  qtopres  23202  fgabs  23383  ptcmplem3  23558  setsmstopn  23986  tngtopn  24167  cnmpopc  24444  pcoval2  24532  pcopt  24538  pcopt2  24539  itgle  25327  ibladdlem  25337  iblabslem  25345  iblabs  25346  iblabsr  25347  iblmulc2  25348  bddiblnc  25359  ditgneg  25374  logbgcd1irr  26299  umgr2adedgspth  29202  n4cyclfrgr  29544  poimirlem26  36514  poimirlem32  36520  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  itg2addnclem  36539  itg2gt0cn  36543  ibladdnclem  36544  iblabsnclem  36551  iblabsnc  36552  iblmulc2nc  36553  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  dicvalrelN  40056  dihvalrel  40150  ldepspr  47154  naryfval  47314  naryfvalixp  47315