Theorem sylan9bb 697

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367

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 369

This theorem is referenced by:  sylan9bbr  698  bi2anan9  871  baibd  907  rbaibd  908  syl3an9b  1295  nanbi12  1355  sbcom2  2193  2sb5rf  2199  2sb6rf  2200  eqeq12  2401  eleq12  2458  sbhypf  3081  ceqsrex2v  3160  sseq12  3440  2ralsng  3981  rexprg  3994  rextpg  3996  breq12  4372  reusv2lem5  4570  opelopabg  4679  brabg  4680  opelopab2  4682  ralxpf  5062  feq23  5624  f00  5675  fconstg  5680  f1oeq23  5718  f1o00  5756  fnelfp  6001  fnelnfp  6003  isofrlem  6137  f1oiso  6148  riota1a  6177  cbvmpt2x  6274  caovord  6385  caovord3  6387  f1oweALT  6683  oaordex  7125  oaass  7128  odi  7146  findcard2s  7676  unfilem1  7699  suppeqfsuppbi  7758  oieu  7879  r1pw  8176  carddomi2  8264  isacn  8338  cdadom2  8480  axdc2  8742  alephval2  8860  fpwwe2cbv  8919  fpwwe2lem2  8921  fpwwecbv  8933  fpwwelem  8934  canthwelem  8939  canthwe  8940  distrlem4pr  9315  axpre-sup  9457  nn0ind-raph  10879  elfz  11599  elfzp12  11679  expeq0  12099  leiso  12412  wrd2ind  12614  trcleq12lem  12831  dfrtrclrec2  12892  shftfib  12907  absdvdsb  14004  dvdsabsb  14005  unbenlem  14428  isprs  15676  isdrs  15680  pltval  15707  lublecllem  15735  istos  15782  isdlat  15940  znfld  18690  tgss2  19574  isopn2  19618  cnpf2  19837  lmbr  19845  isreg2  19964  fclsrest  20610  qustgplem  20704  ustuqtoplem  20827  xmetec  21022  nmogelb  21308  metdstri  21440  tchcph  21765  ulmval  22860  iscgrg  24024  eupath2lem1  25098  eigrei  26869  eigorthi  26872  jplem1  27303  superpos  27389  chrelati  27399  br8d  27597  issiga  28260  eulerpartlemgvv  28498  br8  29351  br6  29352  br4  29353  brsegle  29911  nndivsub  30075  wl-2sb6d  30173  mblfinlem2  30217  cnambfre  30228  itgaddnclem2  30240  ftc1anclem1  30256  topfne  30338  tailfb  30361  filnetlem1  30362  grpokerinj  30513  rngoisoval  30546  smprngopr  30615  rexrabdioph  30893  nzss  31390  iotasbc2  31495  uhg0e  32694  cbvmpt2x2  33125  bj-elequ12  34586  ax12eq  35084  ax12el  35085  2llnjN  35704  2lplnj  35757  elpadd0  35946  lauteq  36232  lpolconN  37627  eliunov2  38218