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  928  sbcom2  2151  sbcom2OLD  2152  sbal1  2171  sbal2  2173  2moOLDOLD  2362  2eu6OLD  2372  mpteq12f  4389  fmptsng  5921  fconstfv  5961  f1oiso  6063  mpt2eq123  6166  tfindsg  6492  findsg  6524  dfoprab4f  6653  opiota  6654  fmpt2x  6661  oalimcl  7020  oeeui  7062  nnmword  7093  isinf  7547  elfi  7684  brwdomn0  7805  alephval3  8301  dfac2  8321  fin17  8584  isfin7-2  8586  ltmpi  9094  addclprlem1  9206  distrlem4pr  9216  1idpr  9219  qreccl  10994  0fz1  11490  zmodid2  11757  hashle00  12179  hashfzdm  12223  hashfirdm  12225  xpnnenOLD  13513  dvdseq  13601  sscntz  15865  gexdvds  16104  cnprest  18915  txrest  19226  ptrescn  19234  flimrest  19578  txflf  19601  fclsrest  19619  tsmssubm  19738  mbfi1fseqlem4  21218  axcontlem7  23238  ubthlem1  24293  pjimai  25602  atcv1  25806  chirredi  25820  wl-sbcom2d-lem1  28411  wl-sbalnae  28414  ptrest  28451  heicant  28452  ftc1anclem1  28493  sbeqi  28998  ralbi12f  28999  iineq12f  29003  raaan2  30025  elovmpt2rab  30184  elovmpt2rab1  30185  ovmpt3rabdm  30188  elovmpt3rab1  30189  hashecclwwlkn1  30534  usghashecclwwlk  30535  numclwlk1lem2fo  30714  snlindsntorlem  31001