Theorem sylan9bbr 693

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 692	. 2 |- ( ( ph /\ th ) -> ( ps <-> ta ) )
4	3	ancoms 450	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  921  sbcomOLD  2118  sbcom2  2153  sbcom2OLD  2154  sbal1  2173  sbal2  2175  2mo  2355  2moOLD  2356  2eu6  2363  mpteq12f  4356  fmptsng  5887  fconstfv  5927  f1oiso  6029  mpt2eq123  6134  tfindsg  6460  findsg  6492  dfoprab4f  6621  opiota  6622  fmpt2x  6629  oalimcl  6987  oeeui  7029  nnmword  7060  isinf  7514  elfi  7651  brwdomn0  7772  alephval3  8268  dfac2  8288  fin17  8551  isfin7-2  8553  ltmpi  9060  addclprlem1  9172  distrlem4pr  9182  1idpr  9185  qreccl  10960  0fz1  11455  zmodid2  11719  hashle00  12141  hashfzdm  12185  hashfirdm  12187  xpnnenOLD  13474  dvdseq  13562  sscntz  15823  gexdvds  16062  cnprest  18734  txrest  19045  ptrescn  19053  flimrest  19397  txflf  19420  fclsrest  19438  tsmssubm  19557  mbfi1fseqlem4  21037  axcontlem7  23038  ubthlem1  24093  pjimai  25402  atcv1  25606  chirredi  25620  wl-sbcom2d-lem1  28231  wl-sbalnae  28234  ptrest  28266  heicant  28267  ftc1anclem1  28308  sbeqi  28813  ralbi12f  28814  raaan2  29842  elovmpt2rab  30001  elovmpt2rab1  30002  ovmpt3rabdm  30005  elovmpt3rab1  30006  hashecclwwlkn1  30351  usghashecclwwlk  30352  numclwlk1lem2fo  30531  snlindsntorlem  30710