Theorem pm2.61d1 172

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 171	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:  ja  174  pm2.61nii  178  pm2.01d  181  moexex  2702  2mo  2712  mosubopt  5159  predpoirr  5915  predfrirr  5916  funfv  6480  dffv2  6486  fvmptnf  6517  rdgsucmptnf  7755  frsucmptn  7764  mapdom2  8364  frfi  8438  oiexg  8673  wemapwe  8835  r1tr  8880  alephsing  9377  uzin  11932  fundmge2nop0  13485  fun2dmnop0  13487  sumrblem  14659  fsumcvg  14660  summolem2a  14663  fsumcvg2  14675  prodeq2ii  14858  prodrblem  14874  fprodcvg  14875  prodmolem2a  14879  zprod  14882  ptpjpre1  21582  qtopres  21709  fgabs  21890  ptcmplem3  22065  setsmstopn  22490  tngtopn  22661  cnmpt2pc  22934  pcoval2  23022  pcopt  23028  pcopt2  23029  itgle  23784  ibladdlem  23794  iblabslem  23802  iblabs  23803  iblabsr  23804  iblmulc2  23805  ditgneg  23829  umgr2adedgspth  27082  n4cyclfrgr  27460  poimirlem26  33742  poimirlem32  33748  ovoliunnfl  33758  voliunnfl  33760  volsupnfl  33761  itg2addnclem  33767  itg2gt0cn  33771  ibladdnclem  33772  iblabsnclem  33779  iblabsnc  33780  iblmulc2nc  33781  bddiblnc  33786  ftc1anclem7  33797  ftc1anclem8  33798  ftc1anc  33799  dicvalrelN  36960  dihvalrel  37054  ldepspr  42824