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  2394  reupick3  3783  difprsnss  4162  pwssun  4786  trin2  5388  fnun  5685  fco  5739  f1co  5788  foco  5803  f1oun  5833  f1oco  5836  eqfnfv  5973  eqfunfv  5978  sorpsscmpl  6573  ordsucsssuc  6636  ordsucun  6638  soxp  6893  ressuppssdif  6918  issmo  7016  tfrlem5  7046  ener  7559  domtr  7565  unen  7595  xpdom2  7609  mapen  7678  unxpdomlem3  7723  fiin  7878  suc11reg  8032  xpnum  8328  pm54.43  8377  r0weon  8386  fseqen  8404  kmlem9  8534  axpre-lttrn  9539  axpre-mulgt0  9541  wloglei  10081  mulnzcnopr  10191  zaddcl  10899  zmulcl  10907  qaddcl  11194  qmulcl  11196  rpaddcl  11236  rpmulcl  11237  rpdivcl  11238  xrltnsym  11339  xrlttri  11341  xmullem  11452  xmulcom  11454  xmulneg1  11457  xmulf  11460  ge0addcl  11628  ge0mulcl  11629  ge0xaddcl  11630  ge0xmulcl  11631  serge0  12125  expclzlem  12154  expge0  12166  expge1  12167  hashfacen  12465  wwlktovf1  12854  xpnnenOLD  13800  qredeu  14103  nn0gcdsq  14140  mul4sq  14327  fpwipodrs  15647  gimco  16111  gictr  16118  symgextf1  16241  efgrelexlemb  16564  xrs1mnd  18224  lmimco  18646  lmictra  18647  iscn2  19505  iscnp2  19506  paste  19561  txuni  19828  txcn  19862  txcmpb  19880  tx2ndc  19887  hmphtr  20019  snfil  20100  supfil  20131  filssufilg  20147  tsmsxp  20392  dscmet  20828  rlimcnp  23023  efnnfsumcl  23104  efchtdvds  23161  lgsne0  23336  mul2sq  23368  colinearalglem2  23886  nb3graprlem2  24128  wlkntrllem3  24239  wlknwwlknsur  24388  wlkiswwlksur  24395  wwlkextinj  24406  frgra3v  24678  ablosn  25025  ablomul  25033  hsn0elch  25842  shscli  25911  hsupss  25935  5oalem6  26253  mdsldmd1i  26926  superpos  26949  ghomsn  28503  sspred  28829  poseq  28910  wfrlem4  28923  frrlem4  28967  sltsolem1  29005  fnsingle  29146  funimage  29155  funpartfun  29170  riscer  29994  divrngidl  30028  mzpincl  30270  kelac2lem  30614  tz6.12-1-afv  31726  bnj110  32995  bj-snsetex  33602  cllem0  36771