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  2627  2mo  2649  mosubopt  5466  predpoirr  6299  predfrirr  6300  funfv  6929  dffv2  6937  fvmptnf  6972  rdgsucmptnf  8370  frsucmptn  8380  mapdom2  9088  frfi  9197  oiexg  9452  wemapwe  9618  r1tr  9700  alephsing  10198  uzin  12799  fundmge2nop0  14437  fun2dmnop0  14439  wrdnfi  14483  relexpsucrd  14968  relexpsucld  14969  relexpreld  14975  relexpdmd  14979  relexprnd  14983  relexpfldd  14985  relexpaddd  14989  dfrtrclrec2  14993  rtrclreclem4  14996  dfrtrcl2  14997  relexpindlem  14998  sumrblem  15646  fsumcvg  15647  summolem2a  15650  fsumcvg2  15662  prodeq2ii  15846  prodrblem  15864  fprodcvg  15865  prodmolem2a  15869  zprod  15872  ptpjpre1  23527  qtopres  23654  fgabs  23835  ptcmplem3  24010  setsmstopn  24434  tngtopn  24606  cnmpopc  24890  pcoval2  24984  pcopt  24990  pcopt2  24991  itgle  25779  ibladdlem  25789  iblabslem  25797  iblabs  25798  iblabsr  25799  iblmulc2  25800  bddiblnc  25811  ditgneg  25826  logbgcd1irr  26772  umgr2adedgspth  30033  n4cyclfrgr  30378  poimirlem26  37891  poimirlem32  37897  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  itg2addnclem  37916  itg2gt0cn  37920  ibladdnclem  37921  iblabsnclem  37928  iblabsnc  37929  iblmulc2nc  37930  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  dicvalrelN  41555  dihvalrel  41649  pgn4cyclex  48480  ldepspr  48827  naryfval  48982  naryfvalixp  48983