Theorem sylan9bbr 698

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 697	. 2 |- ( ( ph /\ th ) -> ( ps <-> ta ) )
4	3	ancoms 451	1 |- ( ( th /\ ph ) -> ( ps <-> ta ) )

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:  pm5.75  935  sbcom2  2193  sbal1  2208  sbal2  2209  2eu6OLD  2315  mpteq12f  4443  fmptsng  5994  fconstfvOLD  6035  f1oiso  6148  mpt2eq123  6255  elovmpt2rab  6420  elovmpt2rab1  6421  ovmpt3rabdm  6434  elovmpt3rab1  6435  tfindsg  6594  findsg  6626  dfoprab4f  6757  opiota  6758  fmpt2x  6765  oalimcl  7127  oeeui  7169  nnmword  7200  isinf  7649  elfi  7788  brwdomn0  7910  alephval3  8404  dfac2  8424  fin17  8687  isfin7-2  8689  ltmpi  9193  addclprlem1  9305  distrlem4pr  9315  1idpr  9318  qreccl  11121  0fz1  11626  zmodid2  11925  hashle00  12369  hashfzdm  12402  hashfirdm  12404  dvdseq  14035  sscntz  16481  gexdvds  16721  cnprest  19876  txrest  20217  ptrescn  20225  flimrest  20569  txflf  20592  fclsrest  20610  tsmssubm  20729  mbfi1fseqlem4  22210  axcontlem7  24394  hashecclwwlkn1  24955  usghashecclwwlk  24956  numclwlk1lem2fo  25216  ubthlem1  25903  pjimai  27211  atcv1  27415  chirredi  27429  wl-sbcom2d-lem1  30174  wl-sbalnae  30177  ptrest  30213  heicant  30214  ftc1anclem1  30256  sbeqi  30734  ralbi12f  30735  iineq12f  30739  nzss  31390  raaan2  32346  uhgeq12g  32688  usgpredgv  32717  usgpredgvALT  32718  rngcinv  32989  rngcinvALTV  33001  ringcinv  33040  ringcinvALTV  33064  snlindsntorlem  33271