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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.61nii  186  ja  188  pm2.01d  192  moexexlem  2651  2mo  2673  mosubopt  5487  predpoirr  6331  predfrirr  6332  funfv  6966  dffv2  6974  fvmptnf  7010  rdgsucmptnf  8419  frsucmptn  8429  mapdom2  9149  frfi  9258  oiexg  9510  wemapwe  9679  r1tr  9761  alephsing  10281  uzin  12926  fundmge2nop0  14570  fun2dmnop0  14572  wrdnfi  14616  relexpsucrd  15109  relexpsucld  15110  relexpreld  15116  relexpdmd  15120  relexprnd  15124  relexpfldd  15126  relexpaddd  15130  dfrtrclrec2  15134  rtrclreclem4  15137  dfrtrcl2  15138  relexpindlem  15139  sumrblem  15800  fsumcvg  15801  summolem2a  15804  fsumcvg2  15816  prodeq2ii  16003  prodrblem  16019  fprodcvg  16020  prodmolem2a  16024  zprod  16027  ptpjpre1  23800  qtopres  23927  fgabs  24108  ptcmplem3  24283  setsmstopn  24707  tngtopn  24879  cnmpopc  25159  pcoval2  25247  pcopt  25253  pcopt2  25254  itgle  26040  ibladdlem  26050  iblabslem  26058  iblabs  26059  iblabsr  26060  iblmulc2  26061  bddiblnc  26072  ditgneg  26087  logbgcd1irr  27034  umgr2adedgspth  30419  n4cyclfrgr  30774  poimirlem26  38398  poimirlem32  38404  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  itg2addnclem  38423  itg2gt0cn  38427  ibladdnclem  38428  iblabsnclem  38435  iblabsnc  38436  iblmulc2nc  38437  ftc1anclem7  38451  ftc1anclem8  38452  ftc1anc  38453  dicvalrelN  42061  dihvalrel  42155  pgn4cyclex  49045  ldepspr  49406  naryfval  49561  naryfvalixp  49562