Theorem syl2anb 482

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

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  sylancb  670  reupick3  3727  difprsnss  4106  pwssun  4739  trin2  5222  sspred  5387  fnun  5680  fco  5737  f1co  5786  foco  5801  f1oun  5831  f1oco  5834  eqfnfv  5974  eqfunfv  5979  sorpsscmpl  6579  ordsucsssuc  6647  ordsucun  6649  soxp  6906  ressuppssdif  6933  wfrlem4  7036  issmo  7064  tfrlem5  7095  ener  7613  domtr  7619  unen  7649  xpdom2  7664  mapen  7733  unxpdomlem3  7775  fiin  7933  suc11reg  8121  xpnum  8382  pm54.43  8431  r0weon  8440  fseqen  8455  kmlem9  8585  axpre-lttrn  9587  axpre-mulgt0  9589  wloglei  10143  mulnzcnopr  10255  zaddcl  10974  zmulcl  10982  qaddcl  11277  qmulcl  11279  rpaddcl  11320  rpmulcl  11321  rpdivcl  11322  xrltnsym  11433  xrlttri  11435  xmullem  11547  xmulcom  11549  xmulneg1  11552  xmulf  11555  ge0addcl  11741  ge0mulcl  11742  ge0xaddcl  11743  ge0xmulcl  11744  serge0  12264  expclzlem  12293  expge0  12305  expge1  12306  hashfacen  12614  wwlktovf1  13025  qredeu  14657  nn0gcdsq  14694  mul4sq  14891  fpwipodrs  16403  gimco  16925  gictr  16932  symgextf1  17055  efgrelexlemb  17393  xrs1mnd  18999  lmimco  19395  lmictra  19396  iscn2  20247  iscnp2  20248  paste  20303  txuni  20600  txcn  20634  txcmpb  20652  tx2ndc  20659  hmphtr  20791  snfil  20872  supfil  20903  filssufilg  20919  tsmsxp  21162  dscmet  21580  rlimcnp  23884  efnnfsumcl  24022  efchtdvds  24079  lgsne0  24254  mul2sq  24286  colinearalglem2  24930  nb3graprlem2  25173  wlkntrllem3  25284  wlknwwlknsur  25433  wlkiswwlksur  25440  wwlkextinj  25451  frgra3v  25723  ablosn  26068  ablomul  26076  hsn0elch  26894  shscli  26963  hsupss  26987  5oalem6  27305  mdsldmd1i  27977  superpos  28000  bnj110  29662  msubco  30162  ghomsn  30299  poseq  30484  frrlem4  30510  sltsolem1  30550  fnsingle  30679  funimage  30688  funpartfun  30703  bj-snsetex  31550  riscer  32220  divrngidl  32254  mzpincl  35570  kelac2lem  35916  rp-fakenanass  36153  cllem0  36164  unhe1  36375  tz6.12-1-afv  38670  nb3grprlem2  39438  cplgr3v  39485  2zrngamgm  39926  2zrngmmgm  39933