Theorem pm2.61d1 183

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 182	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  187  ja  189  pm2.01d  193  moexexlem  2627  2mo  2649  mosubopt  5378  predpoirr  6169  predfrirr  6170  funfv  6776  dffv2  6784  fvmptnf  6818  rdgsucmptnf  8143  frsucmptn  8152  mapdom2  8795  frfi  8894  oiexg  9129  wemapwe  9290  r1tr  9357  alephsing  9855  uzin  12439  fundmge2nop0  14023  fun2dmnop0  14025  wrdnfi  14068  relexpsucrd  14561  relexpsucld  14562  relexpreld  14568  relexpdmd  14572  relexprnd  14576  relexpfldd  14578  relexpaddd  14582  dfrtrclrec2  14586  rtrclreclem4  14589  dfrtrcl2  14590  relexpindlem  14591  sumrblem  15240  fsumcvg  15241  summolem2a  15244  fsumcvg2  15256  prodeq2ii  15438  prodrblem  15454  fprodcvg  15455  prodmolem2a  15459  zprod  15462  ptpjpre1  22422  qtopres  22549  fgabs  22730  ptcmplem3  22905  setsmstopn  23330  tngtopn  23502  cnmpopc  23779  pcoval2  23867  pcopt  23873  pcopt2  23874  itgle  24661  ibladdlem  24671  iblabslem  24679  iblabs  24680  iblabsr  24681  iblmulc2  24682  bddiblnc  24693  ditgneg  24708  logbgcd1irr  25631  umgr2adedgspth  27986  n4cyclfrgr  28328  poimirlem26  35489  poimirlem32  35495  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  itg2addnclem  35514  itg2gt0cn  35518  ibladdnclem  35519  iblabsnclem  35526  iblabsnc  35527  iblmulc2nc  35528  ftc1anclem7  35542  ftc1anclem8  35543  ftc1anc  35544  dicvalrelN  38885  dihvalrel  38979  ldepspr  45430  naryfval  45590  naryfvalixp  45591