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  190  moexexlem  2629  2mo  2651  mosubopt  5529  predpoirr  6365  predfrirr  6366  funfv  7009  dffv2  7017  fvmptnf  7051  rdgsucmptnf  8485  frsucmptn  8495  mapdom2  9214  frfi  9349  oiexg  9604  wemapwe  9766  r1tr  9845  alephsing  10345  uzin  12943  fundmge2nop0  14551  fun2dmnop0  14553  wrdnfi  14596  relexpsucrd  15082  relexpsucld  15083  relexpreld  15089  relexpdmd  15093  relexprnd  15097  relexpfldd  15099  relexpaddd  15103  dfrtrclrec2  15107  rtrclreclem4  15110  dfrtrcl2  15111  relexpindlem  15112  sumrblem  15759  fsumcvg  15760  summolem2a  15763  fsumcvg2  15775  prodeq2ii  15959  prodrblem  15977  fprodcvg  15978  prodmolem2a  15982  zprod  15985  ptpjpre1  23600  qtopres  23727  fgabs  23908  ptcmplem3  24083  setsmstopn  24511  tngtopn  24692  cnmpopc  24974  pcoval2  25068  pcopt  25074  pcopt2  25075  itgle  25865  ibladdlem  25875  iblabslem  25883  iblabs  25884  iblabsr  25885  iblmulc2  25886  bddiblnc  25897  ditgneg  25912  logbgcd1irr  26855  umgr2adedgspth  29981  n4cyclfrgr  30323  poimirlem26  37606  poimirlem32  37612  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem  37631  itg2gt0cn  37635  ibladdnclem  37636  iblabsnclem  37643  iblabsnc  37644  iblmulc2nc  37645  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  dicvalrelN  41142  dihvalrel  41236  ldepspr  48202  naryfval  48362  naryfvalixp  48363