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  2690  2mo  2700  mosubopt  5103  predpoirr  5849  predfrirr  5850  funfv  6405  dffv2  6411  fvmptnf  6442  rdgsucmptnf  7676  frsucmptn  7685  mapdom2  8285  frfi  8359  oiexg  8594  wemapwe  8756  r1tr  8801  alephsing  9298  uzin  11920  fundmge2nop0  13469  fun2dmnop0  13471  sumrblem  14643  fsumcvg  14644  summolem2a  14647  fsumcvg2  14659  prodeq2ii  14843  prodrblem  14859  fprodcvg  14860  prodmolem2a  14864  zprod  14867  ptpjpre1  21588  qtopres  21715  fgabs  21896  ptcmplem3  22071  setsmstopn  22496  tngtopn  22667  cnmpt2pc  22940  pcoval2  23028  pcopt  23034  pcopt2  23035  itgle  23789  ibladdlem  23799  iblabslem  23807  iblabs  23808  iblabsr  23809  iblmulc2  23810  ditgneg  23834  umgr2adedgspth  27088  n4cyclfrgr  27466  poimirlem26  33761  poimirlem32  33767  ovoliunnfl  33777  voliunnfl  33779  volsupnfl  33780  itg2addnclem  33786  itg2gt0cn  33790  ibladdnclem  33791  iblabsnclem  33798  iblabsnc  33799  iblmulc2nc  33800  bddiblnc  33805  ftc1anclem7  33816  ftc1anclem8  33817  ftc1anc  33818  dicvalrelN  36988  dihvalrel  37082  ldepspr  42783