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  2653  2mo  2675  mosubopt  5491  predpoirr  6335  predfrirr  6336  funfv  6969  dffv2  6977  fvmptnf  7013  rdgsucmptnf  8422  frsucmptn  8432  mapdom2  9150  frfi  9259  oiexg  9511  wemapwe  9680  r1tr  9762  alephsing  10282  uzin  12927  fundmge2nop0  14571  fun2dmnop0  14573  wrdnfi  14617  relexpsucrd  15110  relexpsucld  15111  relexpreld  15117  relexpdmd  15121  relexprnd  15125  relexpfldd  15127  relexpaddd  15131  dfrtrclrec2  15135  rtrclreclem4  15138  dfrtrcl2  15139  relexpindlem  15140  sumrblem  15801  fsumcvg  15802  summolem2a  15805  fsumcvg2  15817  prodeq2ii  16004  prodrblem  16022  fprodcvg  16023  prodmolem2a  16027  zprod  16030  ptpjpre1  23803  qtopres  23930  fgabs  24111  ptcmplem3  24286  setsmstopn  24710  tngtopn  24882  cnmpopc  25162  pcoval2  25250  pcopt  25256  pcopt2  25257  itgle  26044  ibladdlem  26054  iblabslem  26062  iblabs  26063  iblabsr  26064  iblmulc2  26065  bddiblnc  26076  ditgneg  26091  logbgcd1irr  27039  umgr2adedgspth  30424  n4cyclfrgr  30779  poimirlem26  38403  poimirlem32  38409  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  itg2addnclem  38428  itg2gt0cn  38432  ibladdnclem  38433  iblabsnclem  38440  iblabsnc  38441  iblmulc2nc  38442  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  dicvalrelN  42066  dihvalrel  42160  pgn4cyclex  49050  ldepspr  49411  naryfval  49566  naryfvalixp  49567