Theorem pm2.61d1 181

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 180	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  185  ja  187  pm2.01d  191  moexexlem  2652  2mo  2674  mosubopt  5478  predpoirr  6316  predfrirr  6317  funfv  6950  dffv2  6958  fvmptnf  6994  rdgsucmptnf  8395  frsucmptn  8405  mapdom2  9116  frfi  9225  oiexg  9480  wemapwe  9649  r1tr  9731  alephsing  10230  uzin  12872  fundmge2nop0  14512  fun2dmnop0  14514  wrdnfi  14558  relexpsucrd  15043  relexpsucld  15044  relexpreld  15050  relexpdmd  15054  relexprnd  15058  relexpfldd  15060  relexpaddd  15064  dfrtrclrec2  15068  rtrclreclem4  15071  dfrtrcl2  15072  relexpindlem  15073  sumrblem  15721  fsumcvg  15722  summolem2a  15725  fsumcvg2  15737  prodeq2ii  15924  prodrblem  15942  fprodcvg  15943  prodmolem2a  15947  zprod  15950  ptpjpre1  23611  qtopres  23738  fgabs  23919  ptcmplem3  24094  setsmstopn  24518  tngtopn  24690  cnmpopc  24970  pcoval2  25058  pcopt  25064  pcopt2  25065  itgle  25852  ibladdlem  25862  iblabslem  25870  iblabs  25871  iblabsr  25872  iblmulc2  25873  bddiblnc  25884  ditgneg  25899  logbgcd1irr  26836  umgr2adedgspth  30094  n4cyclfrgr  30439  poimirlem26  38109  poimirlem32  38115  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  itg2addnclem  38134  itg2gt0cn  38138  ibladdnclem  38139  iblabsnclem  38146  iblabsnc  38147  iblmulc2nc  38148  ftc1anclem7  38162  ftc1anclem8  38163  ftc1anc  38164  dicvalrelN  41773  dihvalrel  41867  pgn4cyclex  48712  ldepspr  49059  naryfval  49214  naryfvalixp  49215