Theorem pm2.61d1 173

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 172	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:  ja  175  pm2.61nii  179  pm2.01d  182  moexexvw  2661  2moswapv  2662  moexex  2669  2mo  2679  mosubopt  5256  predpoirr  6014  predfrirr  6015  funfv  6578  dffv2  6584  fvmptnf  6616  rdgsucmptnf  7869  frsucmptn  7878  mapdom2  8484  frfi  8558  oiexg  8794  wemapwe  8954  r1tr  8999  alephsing  9496  uzin  12092  fundmge2nop0  13661  fun2dmnop0  13663  wrdnfi  13710  sumrblem  14928  fsumcvg  14929  summolem2a  14932  fsumcvg2  14944  prodeq2ii  15127  prodrblem  15143  fprodcvg  15144  prodmolem2a  15148  zprod  15151  ptpjpre1  21883  qtopres  22010  fgabs  22191  ptcmplem3  22366  setsmstopn  22791  tngtopn  22962  cnmpopc  23235  pcoval2  23323  pcopt  23329  pcopt2  23330  itgle  24113  ibladdlem  24123  iblabslem  24131  iblabs  24132  iblabsr  24133  iblmulc2  24134  ditgneg  24158  logbgcd1irr  25073  umgr2adedgspth  27454  n4cyclfrgr  27825  poimirlem26  34365  poimirlem32  34371  ovoliunnfl  34381  voliunnfl  34383  volsupnfl  34384  itg2addnclem  34390  itg2gt0cn  34394  ibladdnclem  34395  iblabsnclem  34402  iblabsnc  34403  iblmulc2nc  34404  bddiblnc  34409  ftc1anclem7  34420  ftc1anclem8  34421  ftc1anc  34422  dicvalrelN  37772  dihvalrel  37866  ldepspr  43901