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  869  baibd  902  rbaibd  903  syl3an9b  1292  nanbi12  1348  sbcom2  2166  sbcom2OLD  2167  2sb5rf  2174  2sb6rf  2175  ax12eq  2257  ax12el  2258  eqeq12  2479  eleq12  2536  sbhypf  3153  ceqsrex2v  3232  sseq12  3520  2ralsng  4057  rexprg  4070  rextpg  4072  breq12  4445  reusv2lem5  4645  opelopabg  4758  brabg  4759  opelopab2  4761  ralxpf  5140  feq23  5707  f00  5758  fconstg  5763  f1oeq23  5801  f1o00  5839  fnelfp  6080  fnelnfp  6082  isofrlem  6215  f1oiso  6226  riota1a  6256  cbvmpt2x  6350  caovord  6461  caovord3  6463  f1oweALT  6758  oaordex  7197  oaass  7200  odi  7218  findcard2s  7750  unfilem1  7773  suppeqfsuppbi  7832  oieu  7953  r1pw  8252  carddomi2  8340  isacn  8414  cdadom2  8556  axdc2  8818  alephval2  8936  fpwwe2cbv  8997  fpwwe2lem2  8999  fpwwecbv  9011  fpwwelem  9012  canthwelem  9017  canthwe  9018  distrlem4pr  9393  axpre-sup  9535  nn0ind-raph  10950  elfz  11667  elfzp12  11746  expeq0  12151  leiso  12461  wrd2ind  12653  shftfib  12855  absdvdsb  13852  dvdsabsb  13853  unbenlem  14274  isprs  15406  isdrs  15410  pltval  15436  lublecllem  15464  istos  15511  isdlat  15669  znfld  18359  tgss2  19248  isopn2  19292  cnpf2  19510  lmbr  19518  isreg2  19637  fclsrest  20253  divstgplem  20347  ustuqtoplem  20470  xmetec  20665  nmogelb  20951  metdstri  21083  tchcph  21408  ulmval  22502  iscgrg  23625  eupath2lem1  24639  eigrei  26415  eigorthi  26418  jplem1  26849  superpos  26935  chrelati  26945  br8d  27122  issiga  27737  eulerpartlemgvv  27941  dfrtrclrec2  28527  br8  28748  br6  28749  br4  28750  brsegle  29321  nndivsub  29485  wl-2sb6d  29571  mblfinlem2  29616  cnambfre  29627  itgaddnclem2  29638  ftc1anclem1  29654  topfne  29749  tailfb  29785  filnetlem1  29786  grpokerinj  29937  rngoisoval  29970  smprngopr  30039  rexrabdioph  30318  iotasbc2  30860  cbvmpt2x2  31864  bj-elequ12  33196  2llnjN  34238  2lplnj  34291  elpadd0  34480  lauteq  34766  lpolconN  36159