Theorem syl2anb 496

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

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  sylancb  699  reupick3  3912  difprsnss  4329  pwssun  5020  trin2  5519  sspred  5688  fundif  5935  fnun  5997  fco  6058  f1co  6110  foco  6125  f1oun  6156  f1oco  6159  eqfnfv  6311  eqfunfv  6316  sorpsscmpl  6948  ordsucsssuc  7023  ordsucun  7025  soxp  7290  ressuppssdif  7316  wfrlem4  7418  issmo  7445  tfrlem5  7476  ener  8002  enerOLD  8003  domtr  8009  unen  8040  xpdom2  8055  mapen  8124  unxpdomlem3  8166  fiin  8328  suc11reg  8516  xpnum  8777  pm54.43  8826  r0weon  8835  fseqen  8850  kmlem9  8980  axpre-lttrn  9987  axpre-mulgt0  9989  wloglei  10560  mulnzcnopr  10673  zaddcl  11417  zmulcl  11426  qaddcl  11804  qmulcl  11806  rpaddcl  11854  rpmulcl  11855  rpdivcl  11856  xrltnsym  11970  xrlttri  11972  xmullem  12094  xmulcom  12096  xmulneg1  12099  xmulf  12102  ge0addcl  12284  ge0mulcl  12285  ge0xaddcl  12286  ge0xmulcl  12287  serge0  12855  expclzlem  12884  expge0  12896  expge1  12897  hashfacen  13238  wwlktovf1  13700  qredeu  15372  nn0gcdsq  15460  mul4sq  15658  fpwipodrs  17164  gimco  17710  gictr  17717  symgextf1  17841  efgrelexlemb  18163  xrs1mnd  19784  lmimco  20183  lmictra  20184  cctop  20810  iscn2  21042  iscnp2  21043  paste  21098  txuni  21395  txcn  21429  txcmpb  21447  tx2ndc  21454  hmphtr  21586  snfil  21668  supfil  21699  filssufilg  21715  tsmsxp  21958  dscmet  22377  rlimcnp  24692  efnnfsumcl  24829  efchtdvds  24885  lgsne0  25060  mul2sq  25144  colinearalglem2  25787  nb3grprlem2  26283  cplgr3v  26331  crctcshwlkn0  26713  wlknwwlksnsur  26776  wlkwwlksur  26783  wwlksnextinj  26794  hsn0elch  28105  shscli  28176  hsupss  28200  5oalem6  28518  mdsldmd1i  29190  superpos  29213  bnj110  30928  msubco  31428  poseq  31750  frrlem4  31783  sltsolem1  31826  fnsingle  32026  funimage  32035  funpartfun  32050  bj-snsetex  32951  bj-snmoore  33068  riscer  33787  divrngidl  33827  mzpincl  37297  kelac2lem  37634  rp-fakenanass  37860  cllem0  37871  unhe1  38079  tz6.12-1-afv  41254  prmdvdsfmtnof1lem2  41497  sprsymrelf1  41746  uspgrsprf1  41755  2zrngamgm  41939  2zrngmmgm  41946