Theorem sylan9bb 692

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 462	. 2 |- ( ( ph /\ th ) -> ( ps <-> ch ) )
3		sylan9bb.2	. . 3 |- ( th -> ( ch <-> ta ) )
4	3	adantl 463	. 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  693  bi2anan9  861  baibd  893  rbaibd  894  syl3an9b  1280  nanbi12  1336  sbcomOLD  2118  sbcom2  2153  sbcom2OLD  2154  2sb5rf  2161  2sb6rf  2162  ax12eq  2243  ax12el  2244  eqeq12  2445  eleq12  2495  sbhypf  3008  ceqsrex2v  3084  sseq12  3367  rexprg  3914  rextpg  3916  breq12  4285  reusv2lem5  4485  opelopabg  4596  brabg  4597  opelopab2  4598  ralxpf  4973  feq23  5533  f00  5581  fconstg  5585  f1oeq23  5623  f1o00  5661  fnelfp  5893  fnelnfp  5895  isofrlem  6018  f1oiso  6029  riota1a  6060  cbvmpt2x  6153  caovord  6263  caovord3  6265  f1oweALT  6550  oaordex  6985  oaass  6988  odi  7006  findcard2s  7541  unfilem1  7564  suppeqfsuppbi  7622  oieu  7741  r1pw  8040  carddomi2  8128  isacn  8202  cdadom2  8344  axdc2  8606  alephval2  8724  fpwwe2cbv  8785  fpwwe2lem2  8787  fpwwecbv  8799  fpwwelem  8800  canthwelem  8805  canthwe  8806  distrlem4pr  9183  axpre-sup  9324  nn0ind-raph  10730  elfz  11430  elfzp12  11523  expeq0  11878  leiso  12196  wrd2ind  12356  shftfib  12545  absdvdsb  13534  dvdsabsb  13535  unbenlem  13952  isprs  15083  isdrs  15087  pltval  15113  lublecllem  15141  istos  15188  isdlat  15346  znfld  17835  tgss2  18434  isopn2  18478  cnpf2  18696  lmbr  18704  isreg2  18823  fclsrest  19439  divstgplem  19533  ustuqtoplem  19656  xmetec  19851  nmogelb  20137  metdstri  20269  tchcph  20594  ulmval  21730  iscgrg  22846  eupath2lem1  23421  eigrei  25061  eigorthi  25064  jplem1  25495  superpos  25581  chrelati  25591  br8d  25766  issiga  26408  eulerpartlemgvv  26607  dfrtrclrec2  27192  br8  27413  br6  27414  br4  27415  brsegle  27986  nndivsub  28151  wl-2sb6d  28232  mblfinlem2  28273  cnambfre  28284  itgaddnclem2  28295  ftc1anclem1  28311  topfne  28406  tailfb  28442  filnetlem1  28443  grpokerinj  28594  rngoisoval  28627  smprngopr  28696  rexrabdioph  28977  iotasbc2  29519  cbvmpt2x2  30570  2llnjN  32784  2lplnj  32837  elpadd0  33026  lauteq  33312  lpolconN  34705