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  2626  2mo  2648  mosubopt  5464  predpoirr  6297  predfrirr  6298  funfv  6927  dffv2  6935  fvmptnf  6970  rdgsucmptnf  8368  frsucmptn  8378  mapdom2  9086  frfi  9195  oiexg  9450  wemapwe  9618  r1tr  9700  alephsing  10198  uzin  12824  fundmge2nop0  14464  fun2dmnop0  14466  wrdnfi  14510  relexpsucrd  14995  relexpsucld  14996  relexpreld  15002  relexpdmd  15006  relexprnd  15010  relexpfldd  15012  relexpaddd  15016  dfrtrclrec2  15020  rtrclreclem4  15023  dfrtrcl2  15024  relexpindlem  15025  sumrblem  15673  fsumcvg  15674  summolem2a  15677  fsumcvg2  15689  prodeq2ii  15876  prodrblem  15894  fprodcvg  15895  prodmolem2a  15899  zprod  15902  ptpjpre1  23536  qtopres  23663  fgabs  23844  ptcmplem3  24019  setsmstopn  24443  tngtopn  24615  cnmpopc  24895  pcoval2  24983  pcopt  24989  pcopt2  24990  itgle  25777  ibladdlem  25787  iblabslem  25795  iblabs  25796  iblabsr  25797  iblmulc2  25798  bddiblnc  25809  ditgneg  25824  logbgcd1irr  26758  umgr2adedgspth  30016  n4cyclfrgr  30361  poimirlem26  37967  poimirlem32  37973  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem  37992  itg2gt0cn  37996  ibladdnclem  37997  iblabsnclem  38004  iblabsnc  38005  iblmulc2nc  38006  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  dicvalrelN  41631  dihvalrel  41725  pgn4cyclex  48602  ldepspr  48949  naryfval  49104  naryfvalixp  49105