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  935  sbcom2  2173  sbcom2OLD  2174  sbal1  2193  sbal2  2195  2moOLDOLD  2384  2eu6OLD  2394  mpteq12f  4523  fmptsng  6082  fconstfv  6123  f1oiso  6235  mpt2eq123  6340  elovmpt2rab  6505  elovmpt2rab1  6506  ovmpt3rabdm  6519  elovmpt3rab1  6520  tfindsg  6679  findsg  6711  dfoprab4f  6842  opiota  6843  fmpt2x  6850  oalimcl  7209  oeeui  7251  nnmword  7282  isinf  7733  elfi  7873  brwdomn0  7995  alephval3  8491  dfac2  8511  fin17  8774  isfin7-2  8776  ltmpi  9282  addclprlem1  9394  distrlem4pr  9404  1idpr  9407  qreccl  11202  0fz1  11705  zmodid2  11992  hashle00  12431  hashfzdm  12464  hashfirdm  12466  xpnnenOLD  13804  dvdseq  13892  sscntz  16169  gexdvds  16410  cnprest  19584  txrest  19895  ptrescn  19903  flimrest  20247  txflf  20270  fclsrest  20288  tsmssubm  20407  mbfi1fseqlem4  21888  axcontlem7  23977  hashecclwwlkn1  24538  usghashecclwwlk  24539  numclwlk1lem2fo  24800  ubthlem1  25490  pjimai  26799  atcv1  27003  chirredi  27017  wl-sbcom2d-lem1  29614  wl-sbalnae  29617  ptrest  29653  heicant  29654  ftc1anclem1  29695  sbeqi  30200  ralbi12f  30201  iineq12f  30205  nzss  30850  raaan2  31675  uhgeq12g  31865  usgpredgv  31894  usgpredgvALT  31895  snlindsntorlem  32170