Theorem syl2anb 487

Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)

Hypotheses

Ref	Expression
syl2anb.1	|- ( ph <-> ps )
syl2anb.2	|- ( ta <-> ch )
syl2anb.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2anb	|- ( ( ph /\ ta ) -> th )

Proof of Theorem syl2anb

Step	Hyp	Ref	Expression
1		syl2anb.2	. 2 |- ( ta <-> ch )
2		syl2anb.1	. . 3 |- ( ph <-> ps )
3		syl2anb.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylanb 480	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 483	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190  df-an 378

This theorem is referenced by:  sylancb  678  reupick3  3719  difprsnss  4098  pwssun  4745  trin2  5229  sspred  5395  fnun  5692  fco  5751  f1co  5801  foco  5816  f1oun  5847  f1oco  5850  eqfnfv  5991  eqfunfv  5996  sorpsscmpl  6601  ordsucsssuc  6669  ordsucun  6671  soxp  6928  ressuppssdif  6955  wfrlem4  7057  issmo  7085  tfrlem5  7116  ener  7634  domtr  7640  unen  7670  xpdom2  7685  mapen  7754  unxpdomlem3  7796  fiin  7954  suc11reg  8142  xpnum  8403  pm54.43  8452  r0weon  8461  fseqen  8476  kmlem9  8606  axpre-lttrn  9608  axpre-mulgt0  9610  wloglei  10167  mulnzcnopr  10280  zaddcl  11001  zmulcl  11009  qaddcl  11303  qmulcl  11305  rpaddcl  11346  rpmulcl  11347  rpdivcl  11348  xrltnsym  11459  xrlttri  11461  xmullem  11575  xmulcom  11577  xmulneg1  11580  xmulf  11583  ge0addcl  11770  ge0mulcl  11771  ge0xaddcl  11772  ge0xmulcl  11773  serge0  12305  expclzlem  12334  expge0  12346  expge1  12347  hashfacen  12658  wwlktovf1  13107  qredeu  14743  nn0gcdsq  14780  mul4sq  14977  fpwipodrs  16488  gimco  17010  gictr  17017  symgextf1  17140  efgrelexlemb  17478  xrs1mnd  19083  lmimco  19479  lmictra  19480  iscn2  20331  iscnp2  20332  paste  20387  txuni  20684  txcn  20718  txcmpb  20736  tx2ndc  20743  hmphtr  20875  snfil  20957  supfil  20988  filssufilg  21004  tsmsxp  21247  dscmet  21665  rlimcnp  23970  efnnfsumcl  24108  efchtdvds  24165  lgsne0  24340  mul2sq  24372  colinearalglem2  25016  nb3graprlem2  25259  wlkntrllem3  25370  wlknwwlknsur  25519  wlkiswwlksur  25526  wwlkextinj  25537  frgra3v  25809  ablosn  26156  ablomul  26164  hsn0elch  26982  shscli  27051  hsupss  27075  5oalem6  27393  mdsldmd1i  28065  superpos  28088  bnj110  29741  msubco  30241  ghomsn  30378  poseq  30562  frrlem4  30588  sltsolem1  30628  fnsingle  30757  funimage  30766  funpartfun  30781  bj-snsetex  31627  riscer  32291  divrngidl  32325  mzpincl  35647  kelac2lem  35993  rp-fakenanass  36230  cllem0  36241  unhe1  36452  tz6.12-1-afv  38821  nb3grprlem2  39619  cplgr3v  39667  crctcsh1wlkn0  39999  2zrngamgm  40447  2zrngmmgm  40454