Theorem syl2anb 477

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

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

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 369

This theorem is referenced by:  sylancb  663  2eu6OLD  2315  reupick3  3708  difprsnss  4079  pwssun  4700  trin2  5303  fnun  5595  fco  5649  f1co  5698  foco  5713  f1oun  5743  f1oco  5746  eqfnfv  5883  eqfunfv  5888  sorpsscmpl  6490  ordsucsssuc  6557  ordsucun  6559  soxp  6812  ressuppssdif  6839  issmo  6937  tfrlem5  6967  ener  7481  domtr  7487  unen  7517  xpdom2  7531  mapen  7600  unxpdomlem3  7642  fiin  7797  suc11reg  7950  xpnum  8245  pm54.43  8294  r0weon  8303  fseqen  8321  kmlem9  8451  axpre-lttrn  9454  axpre-mulgt0  9456  wloglei  10002  mulnzcnopr  10112  zaddcl  10821  zmulcl  10829  qaddcl  11117  qmulcl  11119  rpaddcl  11160  rpmulcl  11161  rpdivcl  11162  xrltnsym  11264  xrlttri  11266  xmullem  11377  xmulcom  11379  xmulneg1  11382  xmulf  11385  ge0addcl  11553  ge0mulcl  11554  ge0xaddcl  11555  ge0xmulcl  11556  serge0  12064  expclzlem  12093  expge0  12105  expge1  12106  hashfacen  12407  wwlktovf1  12806  qredeu  14250  nn0gcdsq  14287  mul4sq  14474  fpwipodrs  15911  gimco  16433  gictr  16440  symgextf1  16563  efgrelexlemb  16885  xrs1mnd  18569  lmimco  18964  lmictra  18965  iscn2  19825  iscnp2  19826  paste  19881  txuni  20178  txcn  20212  txcmpb  20230  tx2ndc  20237  hmphtr  20369  snfil  20450  supfil  20481  filssufilg  20497  tsmsxp  20742  dscmet  21178  rlimcnp  23412  efnnfsumcl  23493  efchtdvds  23550  lgsne0  23725  mul2sq  23757  colinearalglem2  24331  nb3graprlem2  24573  wlkntrllem3  24684  wlknwwlknsur  24833  wlkiswwlksur  24840  wwlkextinj  24851  frgra3v  25123  ablosn  25466  ablomul  25474  hsn0elch  26283  shscli  26352  hsupss  26376  5oalem6  26694  mdsldmd1i  27366  superpos  27389  msubco  29080  ghomsn  29217  sspred  29417  poseq  29498  wfrlem4  29511  frrlem4  29555  sltsolem1  29593  fnsingle  29722  funimage  29731  funpartfun  29746  riscer  30557  divrngidl  30591  mzpincl  30832  kelac2lem  31176  tz6.12-1-afv  32425  2zrngamgm  32945  2zrngmmgm  32952  bnj110  34263  bj-snsetex  34869  rp-fakenanass  38169  cllem0  38180  unhe1  38280