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  189  moexexlem  2622  2mo  2644  mosubopt  5510  predpoirr  6334  predfrirr  6335  funfv  6978  dffv2  6986  fvmptnf  7020  rdgsucmptnf  8428  frsucmptn  8438  mapdom2  9147  frfi  9287  oiexg  9529  wemapwe  9691  r1tr  9770  alephsing  10270  uzin  12861  fundmge2nop0  14452  fun2dmnop0  14454  wrdnfi  14497  relexpsucrd  14979  relexpsucld  14980  relexpreld  14986  relexpdmd  14990  relexprnd  14994  relexpfldd  14996  relexpaddd  15000  dfrtrclrec2  15004  rtrclreclem4  15007  dfrtrcl2  15008  relexpindlem  15009  sumrblem  15656  fsumcvg  15657  summolem2a  15660  fsumcvg2  15672  prodeq2ii  15856  prodrblem  15872  fprodcvg  15873  prodmolem2a  15877  zprod  15880  ptpjpre1  23074  qtopres  23201  fgabs  23382  ptcmplem3  23557  setsmstopn  23985  tngtopn  24166  cnmpopc  24443  pcoval2  24531  pcopt  24537  pcopt2  24538  itgle  25326  ibladdlem  25336  iblabslem  25344  iblabs  25345  iblabsr  25346  iblmulc2  25347  bddiblnc  25358  ditgneg  25373  logbgcd1irr  26296  umgr2adedgspth  29199  n4cyclfrgr  29541  poimirlem26  36509  poimirlem32  36515  ovoliunnfl  36525  voliunnfl  36527  volsupnfl  36528  itg2addnclem  36534  itg2gt0cn  36538  ibladdnclem  36539  iblabsnclem  36546  iblabsnc  36547  iblmulc2nc  36548  ftc1anclem7  36562  ftc1anclem8  36563  ftc1anc  36564  dicvalrelN  40051  dihvalrel  40145  ldepspr  47144  naryfval  47304  naryfvalixp  47305