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  2707  2mo  2729  mosubopt  5392  predpoirr  6170  predfrirr  6171  funfv  6744  dffv2  6750  fvmptnf  6784  rdgsucmptnf  8059  frsucmptn  8068  mapdom2  8682  frfi  8757  oiexg  8993  wemapwe  9154  r1tr  9199  alephsing  9692  uzin  12272  fundmge2nop0  13844  fun2dmnop0  13846  wrdnfi  13893  sumrblem  15062  fsumcvg  15063  summolem2a  15066  fsumcvg2  15078  prodeq2ii  15261  prodrblem  15277  fprodcvg  15278  prodmolem2a  15282  zprod  15285  ptpjpre1  22173  qtopres  22300  fgabs  22481  ptcmplem3  22656  setsmstopn  23082  tngtopn  23253  cnmpopc  23526  pcoval2  23614  pcopt  23620  pcopt2  23621  itgle  24404  ibladdlem  24414  iblabslem  24422  iblabs  24423  iblabsr  24424  iblmulc2  24425  ditgneg  24449  logbgcd1irr  25366  umgr2adedgspth  27721  n4cyclfrgr  28064  poimirlem26  34912  poimirlem32  34918  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  itg2addnclem  34937  itg2gt0cn  34941  ibladdnclem  34942  iblabsnclem  34949  iblabsnc  34950  iblmulc2nc  34951  bddiblnc  34956  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  dicvalrelN  38315  dihvalrel  38409  ldepspr  44522