Theorem pm2.61d1 182

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 181	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  186  ja  188  pm2.01d  192  moexexlem  2711  2mo  2733  mosubopt  5400  predpoirr  6176  predfrirr  6177  funfv  6750  dffv2  6756  fvmptnf  6790  rdgsucmptnf  8065  frsucmptn  8074  mapdom2  8688  frfi  8763  oiexg  8999  wemapwe  9160  r1tr  9205  alephsing  9698  uzin  12279  fundmge2nop0  13851  fun2dmnop0  13853  wrdnfi  13899  sumrblem  15068  fsumcvg  15069  summolem2a  15072  fsumcvg2  15084  prodeq2ii  15267  prodrblem  15283  fprodcvg  15284  prodmolem2a  15288  zprod  15291  ptpjpre1  22179  qtopres  22306  fgabs  22487  ptcmplem3  22662  setsmstopn  23088  tngtopn  23259  cnmpopc  23532  pcoval2  23620  pcopt  23626  pcopt2  23627  itgle  24410  ibladdlem  24420  iblabslem  24428  iblabs  24429  iblabsr  24430  iblmulc2  24431  ditgneg  24455  logbgcd1irr  25372  umgr2adedgspth  27727  n4cyclfrgr  28070  poimirlem26  34933  poimirlem32  34939  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  itg2addnclem  34958  itg2gt0cn  34962  ibladdnclem  34963  iblabsnclem  34970  iblabsnc  34971  iblmulc2nc  34972  bddiblnc  34977  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  dicvalrelN  38336  dihvalrel  38430  ldepspr  44548