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  2372  reupick3  3650  difprsnss  4024  pwssun  4642  trin2  5236  fnun  5532  fco  5583  f1co  5630  foco  5645  f1oun  5675  f1oco  5678  eqfnfv  5812  eqfunfv  5817  sorpsscmpl  6386  ordsucsssuc  6449  ordsucun  6451  soxp  6700  ressuppssdif  6725  issmo  6824  tfrlem5  6854  ener  7371  domtr  7377  unen  7407  xpdom2  7421  mapen  7490  unxpdomlem3  7534  fiin  7687  suc11reg  7840  xpnum  8136  pm54.43  8185  r0weon  8194  fseqen  8212  kmlem9  8342  axpre-lttrn  9348  axpre-mulgt0  9350  wloglei  9887  mulnzcnopr  9997  zaddcl  10700  zmulcl  10708  qaddcl  10984  qmulcl  10986  rpaddcl  11026  rpmulcl  11027  rpdivcl  11028  xrltnsym  11129  xrlttri  11131  xmullem  11242  xmulcom  11244  xmulneg1  11247  xmulf  11250  ge0addcl  11412  ge0mulcl  11413  ge0xaddcl  11414  ge0xmulcl  11415  serge0  11875  expclzlem  11904  expge0  11915  expge1  11916  hashfacen  12222  xpnnenOLD  13507  qredeu  13808  nn0gcdsq  13845  mul4sq  14030  fpwipodrs  15349  gimco  15811  gictr  15818  symgextf1  15941  efgrelexlemb  16262  xrs1mnd  17866  lmimco  18288  lmictra  18289  iscn2  18857  iscnp2  18858  paste  18913  txuni  19180  txcn  19214  txcmpb  19232  tx2ndc  19239  hmphtr  19371  snfil  19452  supfil  19483  filssufilg  19499  tsmsxp  19744  dscmet  20180  rlimcnp  22374  efnnfsumcl  22455  efchtdvds  22512  lgsne0  22687  mul2sq  22719  colinearalglem2  23168  nb3graprlem2  23375  wlkntrllem3  23475  ablosn  23849  ablomul  23857  hsn0elch  24666  shscli  24735  hsupss  24759  5oalem6  25077  mdsldmd1i  25750  superpos  25773  ghomsn  27322  sspred  27648  poseq  27729  wfrlem4  27742  frrlem4  27786  sltsolem1  27824  fnsingle  27965  funimage  27974  funpartfun  27989  riscer  28813  divrngidl  28847  mzpincl  29089  kelac2lem  29436  tz6.12-1-afv  30099  wwlktovf1  30271  wlknwwlknsur  30363  wlkiswwlksur  30370  wwlkextinj  30381  frgra3v  30613  scmatsubcl  30903  scmatmulcl  30905  bnj110  31870  bj-snsetex  32475