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  2652  2mo  2674  mosubopt  5482  mosubott  5484  predpoirr  6329  predfrirr  6330  funfv  6964  dffv2  6972  fvmptnf  7008  rdgsucmptnf  8421  frsucmptn  8431  mapdom2  9151  frfi  9260  oiexg  9513  wemapwe  9682  r1tr  9766  alephsing  10335  uzin  12982  fundmge2nop0  14627  fun2dmnop0  14629  wrdnfi  14673  relexpsucrd  15166  relexpsucld  15167  relexpreld  15173  relexpdmd  15177  relexprnd  15181  relexpfldd  15183  relexpaddd  15187  dfrtrclrec2  15191  rtrclreclem4  15194  dfrtrcl2  15195  relexpindlem  15196  sumrblem  15857  fsumcvg  15858  summolem2a  15861  fsumcvg2  15873  prodeq2ii  16060  prodrblem  16076  fprodcvg  16077  prodmolem2a  16081  zprod  16084  ptpjpre1  23870  qtopres  23997  fgabs  24178  ptcmplem3  24353  setsmstopn  24777  tngtopn  24949  cnmpopc  25229  pcoval2  25317  pcopt  25323  pcopt2  25324  itgle  26110  ibladdlem  26120  iblabslem  26128  iblabs  26129  iblabsr  26130  iblmulc2  26131  bddiblnc  26142  ditgneg  26157  logbgcd1irr  27104  umgr2adedgspth  30519  n4cyclfrgr  30874  poimirlem26  38532  poimirlem32  38538  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  itg2addnclem  38557  itg2gt0cn  38561  ibladdnclem  38562  iblabsnclem  38569  iblabsnc  38570  iblmulc2nc  38571  ftc1anclem7  38585  ftc1anclem8  38586  ftc1anc  38587  dicvalrelN  42210  dihvalrel  42304  pgn4cyclex  49168  ldepspr  49529  naryfval  49684  naryfvalixp  49685