Theorem syl2anb 479

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 472	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2b 475	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  sylancb  665  2eu6OLD  2370  reupick3  3768  difprsnss  4150  pwssun  4776  trin2  5380  fnun  5677  fco  5731  f1co  5780  foco  5795  f1oun  5825  f1oco  5828  eqfnfv  5966  eqfunfv  5971  sorpsscmpl  6576  ordsucsssuc  6643  ordsucun  6645  soxp  6898  ressuppssdif  6923  issmo  7021  tfrlem5  7051  ener  7564  domtr  7570  unen  7600  xpdom2  7614  mapen  7683  unxpdomlem3  7728  fiin  7884  suc11reg  8039  xpnum  8335  pm54.43  8384  r0weon  8393  fseqen  8411  kmlem9  8541  axpre-lttrn  9546  axpre-mulgt0  9548  wloglei  10092  mulnzcnopr  10202  zaddcl  10911  zmulcl  10919  qaddcl  11209  qmulcl  11211  rpaddcl  11251  rpmulcl  11252  rpdivcl  11253  xrltnsym  11354  xrlttri  11356  xmullem  11467  xmulcom  11469  xmulneg1  11472  xmulf  11475  ge0addcl  11643  ge0mulcl  11644  ge0xaddcl  11645  ge0xmulcl  11646  serge0  12143  expclzlem  12172  expge0  12184  expge1  12185  hashfacen  12485  wwlktovf1  12877  xpnnenOLD  13925  qredeu  14230  nn0gcdsq  14267  mul4sq  14454  fpwipodrs  15773  gimco  16295  gictr  16302  symgextf1  16425  efgrelexlemb  16747  xrs1mnd  18435  lmimco  18857  lmictra  18858  iscn2  19717  iscnp2  19718  paste  19773  txuni  20071  txcn  20105  txcmpb  20123  tx2ndc  20130  hmphtr  20262  snfil  20343  supfil  20374  filssufilg  20390  tsmsxp  20635  dscmet  21071  rlimcnp  23273  efnnfsumcl  23354  efchtdvds  23411  lgsne0  23586  mul2sq  23618  colinearalglem2  24188  nb3graprlem2  24430  wlkntrllem3  24541  wlknwwlknsur  24690  wlkiswwlksur  24697  wwlkextinj  24708  frgra3v  24980  ablosn  25327  ablomul  25335  hsn0elch  26144  shscli  26213  hsupss  26237  5oalem6  26555  mdsldmd1i  27228  superpos  27251  msubco  28869  ghomsn  29006  sspred  29228  poseq  29309  wfrlem4  29322  frrlem4  29366  sltsolem1  29404  fnsingle  29545  funimage  29554  funpartfun  29569  riscer  30367  divrngidl  30401  mzpincl  30642  kelac2lem  30986  tz6.12-1-afv  32213  2zrngamgm  32572  2zrngmmgm  32579  bnj110  33784  bj-snsetex  34404  rp-fakenanass  37577  cllem0  37589  unhe1  37630