Theorem sylan9bb 699

Description: Nested syllogism inference conjoining dissimilar antecedents. (Contributed by NM, 4-Mar-1995.)

Hypotheses

Ref	Expression
sylan9bb.1	|- ( ph -> ( ps <-> ch ) )
sylan9bb.2	|- ( th -> ( ch <-> ta ) )

Assertion

Ref	Expression
sylan9bb	|- ( ( ph /\ th ) -> ( ps <-> ta ) )

Proof of Theorem sylan9bb

Step	Hyp	Ref	Expression
1		sylan9bb.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 465	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 466	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 253	1 |- ( ( ph /\ th ) -> ( 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:  sylan9bbr  700  bi2anan9  873  baibd  909  rbaibd  910  syl3an9b  1298  nanbi12  1357  sbcom2  2175  2sb5rf  2181  2sb6rf  2182  ax12eq  2257  ax12el  2258  eqeq12  2462  eleq12  2519  sbhypf  3142  ceqsrex2v  3221  sseq12  3512  2ralsng  4051  rexprg  4064  rextpg  4066  breq12  4442  reusv2lem5  4642  opelopabg  4755  brabg  4756  opelopab2  4758  ralxpf  5139  feq23  5706  f00  5757  fconstg  5762  f1oeq23  5800  f1o00  5838  fnelfp  6084  fnelnfp  6086  isofrlem  6221  f1oiso  6232  riota1a  6262  cbvmpt2x  6360  caovord  6471  caovord3  6473  f1oweALT  6769  oaordex  7209  oaass  7212  odi  7230  findcard2s  7763  unfilem1  7786  suppeqfsuppbi  7845  oieu  7967  r1pw  8266  carddomi2  8354  isacn  8428  cdadom2  8570  axdc2  8832  alephval2  8950  fpwwe2cbv  9011  fpwwe2lem2  9013  fpwwecbv  9025  fpwwelem  9026  canthwelem  9031  canthwe  9032  distrlem4pr  9407  axpre-sup  9549  nn0ind-raph  10969  elfz  11687  elfzp12  11766  expeq0  12175  leiso  12487  wrd2ind  12682  shftfib  12884  absdvdsb  13879  dvdsabsb  13880  unbenlem  14303  isprs  15433  isdrs  15437  pltval  15464  lublecllem  15492  istos  15539  isdlat  15697  znfld  18472  tgss2  19362  isopn2  19406  cnpf2  19624  lmbr  19632  isreg2  19751  fclsrest  20398  qustgplem  20492  ustuqtoplem  20615  xmetec  20810  nmogelb  21096  metdstri  21228  tchcph  21553  ulmval  22647  iscgrg  23776  eupath2lem1  24849  eigrei  26625  eigorthi  26628  jplem1  27059  superpos  27145  chrelati  27155  br8d  27335  issiga  27984  eulerpartlemgvv  28188  dfrtrclrec2  28939  br8  29160  br6  29161  br4  29162  brsegle  29733  nndivsub  29897  wl-2sb6d  29983  mblfinlem2  30027  cnambfre  30038  itgaddnclem2  30049  ftc1anclem1  30065  topfne  30147  tailfb  30170  filnetlem1  30171  grpokerinj  30322  rngoisoval  30355  smprngopr  30424  rexrabdioph  30702  nzss  31198  iotasbc2  31281  uhg0e  32214  cbvmpt2x2  32658  bj-elequ12  33987  2llnjN  35031  2lplnj  35084  elpadd0  35273  lauteq  35559  lpolconN  36954