Theorem sylan9bb 736

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 481	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 482	. 2 |- ( ( ph /\ th ) -> ( ch <-> ta ) )
5	2, 4	bitrd 268	1 |- ( ( ph /\ th ) -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  sylan9bbr  737  bi2anan9  917  baibd  948  rbaibd  949  syl3an9b  1397  nanbi12  1457  sbcom2  2445  2sb5rf  2451  2sb6rf  2452  eqeq12  2635  eleq12  2691  sbhypf  3253  ceqsrex2v  3338  sseq12  3628  2ralsng  4220  rexprg  4235  rextpg  4237  breq12  4658  reusv2lem5  4873  opelopabg  4993  brabg  4994  opelopabgf  4995  opelopab2  4996  rbropapd  5015  ralxpf  5268  feq23  6029  f00  6087  fconstg  6092  f1oeq23  6130  f1o00  6171  fnelfp  6441  fnelnfp  6443  isofrlem  6590  f1oiso  6601  riota1a  6630  cbvmpt2x  6733  caovord  6845  caovord3  6847  f1oweALT  7152  oaordex  7638  oaass  7641  odi  7659  findcard2s  8201  unfilem1  8224  suppeqfsuppbi  8289  oieu  8444  r1pw  8708  carddomi2  8796  isacn  8867  cdadom2  9009  axdc2  9271  alephval2  9394  fpwwe2cbv  9452  fpwwe2lem2  9454  fpwwecbv  9466  fpwwelem  9467  canthwelem  9472  canthwe  9473  distrlem4pr  9848  axpre-sup  9990  nn0ind-raph  11477  xnn0xadd0  12077  elfz  12332  elfzp12  12419  expeq0  12890  leiso  13243  wrd2ind  13477  trcleq12lem  13732  dfrtrclrec2  13797  shftfib  13812  absdvdsb  15000  dvdsabsb  15001  dvdsabseq  15035  unbenlem  15612  isprs  16930  isdrs  16934  pltval  16960  lublecllem  16988  istos  17035  isdlat  17193  znfld  19909  tgss2  20791  isopn2  20836  cnpf2  21054  lmbr  21062  isreg2  21181  fclsrest  21828  qustgplem  21924  ustuqtoplem  22043  xmetec  22239  nmogelb  22520  metdstri  22654  tchcph  23036  ulmval  24134  2lgslem1a  25116  iscgrg  25407  istrlson  26603  ispthson  26638  isspthson  26639  elwwlks2on  26852  eupth2lem1  27078  eigrei  28693  eigorthi  28696  jplem1  29127  superpos  29213  chrelati  29223  vtocl2d  29314  br8d  29422  issiga  30174  eulerpartlemgvv  30438  br8  31646  br6  31647  br4  31648  brsegle  32215  topfne  32349  tailfb  32372  filnetlem1  32373  nndivsub  32456  bj-elequ12  32668  bj-rest10  33041  isbasisrelowllem1  33203  isbasisrelowllem2  33204  wl-2sb6d  33341  curf  33387  curunc  33391  poimirlem26  33435  mblfinlem2  33447  cnambfre  33458  itgaddnclem2  33469  ftc1anclem1  33485  grpokerinj  33692  rngoisoval  33776  smprngopr  33851  ax12eq  34226  ax12el  34227  2llnjN  34853  2lplnj  34906  elpadd0  35095  lauteq  35381  lpolconN  36776  rexrabdioph  37358  eliunov2  37971  nzss  38516  iotasbc2  38621  cbvmpt2x2  42114