Theorem sylan9bbr 712

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

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm5.75  953  pm5.75OLD  954  sbcom2  2285  sbal1  2300  sbal2  2301  mpteq12f  4493  fmptsng  6109  fconstfvOLD  6152  f1oiso  6267  mpt2eq123  6377  elovmpt2rab  6542  elovmpt2rab1  6543  ovmpt3rabdm  6553  elovmpt3rab1  6554  tfindsg  6714  findsg  6747  dfoprab4f  6878  opiota  6879  fmpt2x  6886  oalimcl  7287  oeeui  7329  nnmword  7360  isinf  7811  elfi  7953  brwdomn0  8110  alephval3  8567  dfac2  8587  fin17  8850  isfin7-2  8852  ltmpi  9355  addclprlem1  9467  distrlem4pr  9477  1idpr  9480  qreccl  11313  0fz1  11848  zmodid2  12157  hashle00  12609  hashfzdm  12645  hashfirdm  12647  dvdseq  14401  sscntz  17029  gexdvds  17284  cnprest  20354  txrest  20695  ptrescn  20703  flimrest  21047  txflf  21070  fclsrest  21088  tsmssubm  21206  mbfi1fseqlem4  22725  axcontlem7  25049  hashecclwwlkn1  25611  usghashecclwwlk  25612  numclwlk1lem2fo  25872  ubthlem1  26561  pjimai  27878  atcv1  28082  chirredi  28096  wl-sbcom2d-lem1  31934  wl-sbalnae  31937  ptrest  31984  poimirlem28  32013  heicant  32020  ftc1anclem1  32062  sbeqi  32448  ralbi12f  32449  iineq12f  32453  nzss  36710  raaan2  38634  uhgreq12g  39202  nbuhgr2vtx1edgb  39470  1wlkcomp  39692  uhgr1wlkspthlem2  39786  clWlkcomp  39805  uhgeq12gALTV  39955  usgpredgv  39984  usgpredgvALT  39985  rngcinv  40256  rngcinvALTV  40268  ringcinv  40307  ringcinvALTV  40331  snlindsntorlem  40536