Theorem pm2.61d1 170

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 169	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  172  pm2.61nii  177  pm2.01d  180  moexex  2529  2mo  2539  mosubopt  4897  predpoirr  5625  predfrirr  5626  funfv  6175  dffv2  6181  fvmptnf  6210  rdgsucmptnf  7412  frsucmptn  7421  mapdom2  8016  frfi  8090  oiexg  8323  wemapwe  8477  r1tr  8522  alephsing  8981  uzin  11596  fundmge2nop0  13129  fun2dmnop0  13131  sumrblem  14289  fsumcvg  14290  summolem2a  14293  fsumcvg2  14305  prodeq2ii  14482  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  zprod  14506  ptpjpre1  21184  qtopres  21311  fgabs  21493  ptcmplem3  21668  setsmstopn  22093  tngtopn  22264  cnmpt2pc  22535  pcoval2  22624  pcopt  22630  pcopt2  22631  itgle  23382  ibladdlem  23392  iblabslem  23400  iblabs  23401  iblabsr  23402  iblmulc2  23403  ditgneg  23427  nbgra0nb  25958  n4cyclfrgra  26545  poimirlem26  32605  poimirlem32  32611  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  itg2addnclem  32631  itg2gt0cn  32635  ibladdnclem  32636  iblabsnclem  32643  iblabsnc  32644  iblmulc2nc  32645  bddiblnc  32650  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  dicvalrelN  35492  dihvalrel  35586  umgr2adedgspth  41155  n4cyclfrgr  41461  ldepspr  42056