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  2628  2mo  2650  mosubopt  5418  predpoirr  6225  predfrirr  6226  funfv  6837  dffv2  6845  fvmptnf  6879  rdgsucmptnf  8231  frsucmptn  8240  mapdom2  8884  frfi  8989  oiexg  9224  wemapwe  9385  r1tr  9465  alephsing  9963  uzin  12547  fundmge2nop0  14134  fun2dmnop0  14136  wrdnfi  14179  relexpsucrd  14672  relexpsucld  14673  relexpreld  14679  relexpdmd  14683  relexprnd  14687  relexpfldd  14689  relexpaddd  14693  dfrtrclrec2  14697  rtrclreclem4  14700  dfrtrcl2  14701  relexpindlem  14702  sumrblem  15351  fsumcvg  15352  summolem2a  15355  fsumcvg2  15367  prodeq2ii  15551  prodrblem  15567  fprodcvg  15568  prodmolem2a  15572  zprod  15575  ptpjpre1  22630  qtopres  22757  fgabs  22938  ptcmplem3  23113  setsmstopn  23539  tngtopn  23720  cnmpopc  23997  pcoval2  24085  pcopt  24091  pcopt2  24092  itgle  24879  ibladdlem  24889  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  bddiblnc  24911  ditgneg  24926  logbgcd1irr  25849  umgr2adedgspth  28214  n4cyclfrgr  28556  poimirlem26  35730  poimirlem32  35736  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnclem  35755  itg2gt0cn  35759  ibladdnclem  35760  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  dicvalrelN  39126  dihvalrel  39220  ldepspr  45702  naryfval  45862  naryfvalixp  45863