Theorem sylan9bbr 700

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bbr.1	|- ( ph -> ( ps <-> ch ) )
sylan9bbr.2	|- ( th -> ( ch <-> ta ) )

Assertion

Ref	Expression
sylan9bbr	|- ( ( th /\ ph ) -> ( ps <-> ta ) )

Proof of Theorem sylan9bbr

Step	Hyp	Ref	Expression
1		sylan9bbr.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		sylan9bbr.2	. . 3 |- ( th -> ( ch <-> ta ) )
3	1, 2	sylan9bb 699	. 2 |- ( ( ph /\ th ) -> ( ps <-> ta ) )
4	3	ancoms 453	1 |- ( ( th /\ ph ) -> ( ps <-> ta ) )

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:  pm5.75  937  sbcom2  2175  sbal1  2190  sbal2  2191  2eu6OLD  2370  mpteq12f  4513  fmptsng  6077  fconstfvOLD  6119  f1oiso  6232  mpt2eq123  6341  elovmpt2rab  6506  elovmpt2rab1  6507  ovmpt3rabdm  6520  elovmpt3rab1  6521  tfindsg  6680  findsg  6712  dfoprab4f  6843  opiota  6844  fmpt2x  6851  oalimcl  7211  oeeui  7253  nnmword  7284  isinf  7735  elfi  7875  brwdomn0  7998  alephval3  8494  dfac2  8514  fin17  8777  isfin7-2  8779  ltmpi  9285  addclprlem1  9397  distrlem4pr  9407  1idpr  9410  qreccl  11213  0fz1  11716  zmodid2  12006  hashle00  12447  hashfzdm  12480  hashfirdm  12482  xpnnenOLD  13925  dvdseq  14015  sscntz  16343  gexdvds  16583  cnprest  19768  txrest  20110  ptrescn  20118  flimrest  20462  txflf  20485  fclsrest  20503  tsmssubm  20622  mbfi1fseqlem4  22103  axcontlem7  24251  hashecclwwlkn1  24812  usghashecclwwlk  24813  numclwlk1lem2fo  25073  ubthlem1  25764  pjimai  27073  atcv1  27277  chirredi  27291  wl-sbcom2d-lem1  29985  wl-sbalnae  29988  ptrest  30024  heicant  30025  ftc1anclem1  30066  sbeqi  30544  ralbi12f  30545  iineq12f  30549  nzss  31198  raaan2  32134  uhgeq12g  32324  usgpredgv  32353  usgpredgvALT  32354  rngcinv  32664  rngcinvOLD  32676  ringcinv  32712  ringcinvOLD  32736  snlindsntorlem  32941