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  2621  2mo  2643  mosubopt  5450  predpoirr  6280  predfrirr  6281  funfv  6909  dffv2  6917  fvmptnf  6951  rdgsucmptnf  8348  frsucmptn  8358  mapdom2  9061  frfi  9169  oiexg  9421  wemapwe  9587  r1tr  9669  alephsing  10167  uzin  12772  fundmge2nop0  14409  fun2dmnop0  14411  wrdnfi  14455  relexpsucrd  14940  relexpsucld  14941  relexpreld  14947  relexpdmd  14951  relexprnd  14955  relexpfldd  14957  relexpaddd  14961  dfrtrclrec2  14965  rtrclreclem4  14968  dfrtrcl2  14969  relexpindlem  14970  sumrblem  15618  fsumcvg  15619  summolem2a  15622  fsumcvg2  15634  prodeq2ii  15818  prodrblem  15836  fprodcvg  15837  prodmolem2a  15841  zprod  15844  ptpjpre1  23487  qtopres  23614  fgabs  23795  ptcmplem3  23970  setsmstopn  24394  tngtopn  24566  cnmpopc  24850  pcoval2  24944  pcopt  24950  pcopt2  24951  itgle  25739  ibladdlem  25749  iblabslem  25757  iblabs  25758  iblabsr  25759  iblmulc2  25760  bddiblnc  25771  ditgneg  25786  logbgcd1irr  26732  umgr2adedgspth  29927  n4cyclfrgr  30269  poimirlem26  37692  poimirlem32  37698  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  itg2addnclem  37717  itg2gt0cn  37721  ibladdnclem  37722  iblabsnclem  37729  iblabsnc  37730  iblmulc2nc  37731  ftc1anclem7  37745  ftc1anclem8  37746  ftc1anc  37747  dicvalrelN  41230  dihvalrel  41324  pgn4cyclex  48163  ldepspr  48511  naryfval  48666  naryfvalixp  48667