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  2623  2mo  2645  mosubopt  5519  predpoirr  6355  predfrirr  6356  funfv  6995  dffv2  7003  fvmptnf  7037  rdgsucmptnf  8467  frsucmptn  8477  mapdom2  9186  frfi  9318  oiexg  9572  wemapwe  9734  r1tr  9813  alephsing  10313  uzin  12915  fundmge2nop0  14537  fun2dmnop0  14539  wrdnfi  14582  relexpsucrd  15068  relexpsucld  15069  relexpreld  15075  relexpdmd  15079  relexprnd  15083  relexpfldd  15085  relexpaddd  15089  dfrtrclrec2  15093  rtrclreclem4  15096  dfrtrcl2  15097  relexpindlem  15098  sumrblem  15743  fsumcvg  15744  summolem2a  15747  fsumcvg2  15759  prodeq2ii  15943  prodrblem  15961  fprodcvg  15962  prodmolem2a  15966  zprod  15969  ptpjpre1  23594  qtopres  23721  fgabs  23902  ptcmplem3  24077  setsmstopn  24505  tngtopn  24686  cnmpopc  24968  pcoval2  25062  pcopt  25068  pcopt2  25069  itgle  25859  ibladdlem  25869  iblabslem  25877  iblabs  25878  iblabsr  25879  iblmulc2  25880  bddiblnc  25891  ditgneg  25906  logbgcd1irr  26851  umgr2adedgspth  29977  n4cyclfrgr  30319  poimirlem26  37632  poimirlem32  37638  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnclem  37657  itg2gt0cn  37661  ibladdnclem  37662  iblabsnclem  37669  iblabsnc  37670  iblmulc2nc  37671  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  dicvalrelN  41167  dihvalrel  41261  ldepspr  48318  naryfval  48477  naryfvalixp  48478