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  2615  2mo  2637  mosubopt  5516  predpoirr  6346  predfrirr  6347  funfv  6989  dffv2  6997  fvmptnf  7031  rdgsucmptnf  8459  frsucmptn  8469  mapdom2  9186  frfi  9322  oiexg  9578  wemapwe  9740  r1tr  9819  alephsing  10319  uzin  12914  fundmge2nop0  14511  fun2dmnop0  14513  wrdnfi  14556  relexpsucrd  15038  relexpsucld  15039  relexpreld  15045  relexpdmd  15049  relexprnd  15053  relexpfldd  15055  relexpaddd  15059  dfrtrclrec2  15063  rtrclreclem4  15066  dfrtrcl2  15067  relexpindlem  15068  sumrblem  15715  fsumcvg  15716  summolem2a  15719  fsumcvg2  15731  prodeq2ii  15915  prodrblem  15931  fprodcvg  15932  prodmolem2a  15936  zprod  15939  ptpjpre1  23566  qtopres  23693  fgabs  23874  ptcmplem3  24049  setsmstopn  24477  tngtopn  24658  cnmpopc  24940  pcoval2  25034  pcopt  25040  pcopt2  25041  itgle  25830  ibladdlem  25840  iblabslem  25848  iblabs  25849  iblabsr  25850  iblmulc2  25851  bddiblnc  25862  ditgneg  25877  logbgcd1irr  26822  umgr2adedgspth  29882  n4cyclfrgr  30224  poimirlem26  37347  poimirlem32  37353  ovoliunnfl  37363  voliunnfl  37365  volsupnfl  37366  itg2addnclem  37372  itg2gt0cn  37376  ibladdnclem  37377  iblabsnclem  37384  iblabsnc  37385  iblmulc2nc  37386  ftc1anclem7  37400  ftc1anclem8  37401  ftc1anc  37402  dicvalrelN  40884  dihvalrel  40978  ldepspr  47856  naryfval  48016  naryfvalixp  48017