Theorem sylan9bbr 705

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

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm5.75  945  sbcom2  2241  sbal1  2256  sbal2  2257  2eu6OLD  2362  mpteq12f  4502  fmptsng  6100  fconstfvOLD  6142  f1oiso  6257  mpt2eq123  6364  elovmpt2rab  6529  elovmpt2rab1  6530  ovmpt3rabdm  6540  elovmpt3rab1  6541  tfindsg  6701  findsg  6734  dfoprab4f  6865  opiota  6866  fmpt2x  6873  oalimcl  7269  oeeui  7311  nnmword  7342  isinf  7791  elfi  7933  brwdomn0  8084  alephval3  8539  dfac2  8559  fin17  8822  isfin7-2  8824  ltmpi  9328  addclprlem1  9440  distrlem4pr  9450  1idpr  9453  qreccl  11284  0fz1  11817  zmodid2  12122  hashle00  12574  hashfzdm  12607  hashfirdm  12609  dvdseq  14330  sscntz  16922  gexdvds  17162  cnprest  20227  txrest  20568  ptrescn  20576  flimrest  20920  txflf  20943  fclsrest  20961  tsmssubm  21079  mbfi1fseqlem4  22544  axcontlem7  24837  hashecclwwlkn1  25398  usghashecclwwlk  25399  numclwlk1lem2fo  25659  ubthlem1  26348  pjimai  27655  atcv1  27859  chirredi  27873  wl-sbcom2d-lem1  31587  wl-sbalnae  31590  ptrest  31633  poimirlem28  31662  heicant  31669  ftc1anclem1  31711  sbeqi  32097  ralbi12f  32098  iineq12f  32102  nzss  36293  raaan2  37977  uhgeq12g  38430  usgpredgv  38459  usgpredgvALT  38460  rngcinv  38731  rngcinvALTV  38743  ringcinv  38782  ringcinvALTV  38806  snlindsntorlem  39013