Theorem pm2.61d1 180

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 179	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  184  ja  186  pm2.01d  190  moexexlem  2626  2mo  2648  mosubopt  5458  predpoirr  6291  predfrirr  6292  funfv  6921  dffv2  6929  fvmptnf  6963  rdgsucmptnf  8360  frsucmptn  8370  mapdom2  9076  frfi  9185  oiexg  9440  wemapwe  9606  r1tr  9688  alephsing  10186  uzin  12787  fundmge2nop0  14425  fun2dmnop0  14427  wrdnfi  14471  relexpsucrd  14956  relexpsucld  14957  relexpreld  14963  relexpdmd  14967  relexprnd  14971  relexpfldd  14973  relexpaddd  14977  dfrtrclrec2  14981  rtrclreclem4  14984  dfrtrcl2  14985  relexpindlem  14986  sumrblem  15634  fsumcvg  15635  summolem2a  15638  fsumcvg2  15650  prodeq2ii  15834  prodrblem  15852  fprodcvg  15853  prodmolem2a  15857  zprod  15860  ptpjpre1  23515  qtopres  23642  fgabs  23823  ptcmplem3  23998  setsmstopn  24422  tngtopn  24594  cnmpopc  24878  pcoval2  24972  pcopt  24978  pcopt2  24979  itgle  25767  ibladdlem  25777  iblabslem  25785  iblabs  25786  iblabsr  25787  iblmulc2  25788  bddiblnc  25799  ditgneg  25814  logbgcd1irr  26760  umgr2adedgspth  30021  n4cyclfrgr  30366  poimirlem26  37843  poimirlem32  37849  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  itg2addnclem  37868  itg2gt0cn  37872  ibladdnclem  37873  iblabsnclem  37880  iblabsnc  37881  iblmulc2nc  37882  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  dicvalrelN  41441  dihvalrel  41535  pgn4cyclex  48368  ldepspr  48715  naryfval  48870  naryfvalixp  48871