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  2619  2mo  2641  mosubopt  5457  predpoirr  6285  predfrirr  6286  funfv  6914  dffv2  6922  fvmptnf  6956  rdgsucmptnf  8358  frsucmptn  8368  mapdom2  9072  frfi  9190  oiexg  9446  wemapwe  9612  r1tr  9691  alephsing  10189  uzin  12793  fundmge2nop0  14427  fun2dmnop0  14429  wrdnfi  14473  relexpsucrd  14958  relexpsucld  14959  relexpreld  14965  relexpdmd  14969  relexprnd  14973  relexpfldd  14975  relexpaddd  14979  dfrtrclrec2  14983  rtrclreclem4  14986  dfrtrcl2  14987  relexpindlem  14988  sumrblem  15636  fsumcvg  15637  summolem2a  15640  fsumcvg2  15652  prodeq2ii  15836  prodrblem  15854  fprodcvg  15855  prodmolem2a  15859  zprod  15862  ptpjpre1  23474  qtopres  23601  fgabs  23782  ptcmplem3  23957  setsmstopn  24382  tngtopn  24554  cnmpopc  24838  pcoval2  24932  pcopt  24938  pcopt2  24939  itgle  25727  ibladdlem  25737  iblabslem  25745  iblabs  25746  iblabsr  25747  iblmulc2  25748  bddiblnc  25759  ditgneg  25774  logbgcd1irr  26720  umgr2adedgspth  29911  n4cyclfrgr  30253  poimirlem26  37625  poimirlem32  37631  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  itg2addnclem  37650  itg2gt0cn  37654  ibladdnclem  37655  iblabsnclem  37662  iblabsnc  37663  iblmulc2nc  37664  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  dicvalrelN  41164  dihvalrel  41258  pgn4cyclex  48111  ldepspr  48459  naryfval  48614  naryfvalixp  48615