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  2620  2mo  2642  mosubopt  5473  predpoirr  6309  predfrirr  6310  funfv  6951  dffv2  6959  fvmptnf  6993  rdgsucmptnf  8400  frsucmptn  8410  mapdom2  9118  frfi  9239  oiexg  9495  wemapwe  9657  r1tr  9736  alephsing  10236  uzin  12840  fundmge2nop0  14474  fun2dmnop0  14476  wrdnfi  14520  relexpsucrd  15006  relexpsucld  15007  relexpreld  15013  relexpdmd  15017  relexprnd  15021  relexpfldd  15023  relexpaddd  15027  dfrtrclrec2  15031  rtrclreclem4  15034  dfrtrcl2  15035  relexpindlem  15036  sumrblem  15684  fsumcvg  15685  summolem2a  15688  fsumcvg2  15700  prodeq2ii  15884  prodrblem  15902  fprodcvg  15903  prodmolem2a  15907  zprod  15910  ptpjpre1  23465  qtopres  23592  fgabs  23773  ptcmplem3  23948  setsmstopn  24373  tngtopn  24545  cnmpopc  24829  pcoval2  24923  pcopt  24929  pcopt2  24930  itgle  25718  ibladdlem  25728  iblabslem  25736  iblabs  25737  iblabsr  25738  iblmulc2  25739  bddiblnc  25750  ditgneg  25765  logbgcd1irr  26711  umgr2adedgspth  29885  n4cyclfrgr  30227  poimirlem26  37647  poimirlem32  37653  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnclem  37672  itg2gt0cn  37676  ibladdnclem  37677  iblabsnclem  37684  iblabsnc  37685  iblmulc2nc  37686  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  dicvalrelN  41186  dihvalrel  41280  pgn4cyclex  48120  ldepspr  48466  naryfval  48621  naryfvalixp  48622