Theorem syl6rbbr 538

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

Ref	Expression
syl6rbbr	|- (ph -> (th <-> ps))

Proof of Theorem syl6rbbr

Step	Hyp	Ref	Expression
1		syl6rbbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl6rbbr.2	. . 3 |- (th <-> ch)
3	2	bicomi 172	. 2 |- (ch <-> th)
4	1, 3	syl6rbb 536	1 |- (ph -> (th <-> ps))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  baib 684  reu8 1932  sbcgf 1982  sbcel12g 2007  disjssun 2322  r19.28zv 2346  r19.37zv 2347  r19.45zv 2348  r19.27zv 2349  r19.36zv 2350  ralidm 2353  iunconst 2567  elpwun 2906  dfom2 3128  funssres 3544  fncnv 3553  fcoi1 3636  fcoi2 3637  funimass4 3754  dffo3 3810  funfvima 3843  isomin 3890  f1oweALT 3897  tz7.48-2 3948  eloprabg 3998  oe0m1 4150  pw2en 4432  xpmapenlem4 4485  aceq3 4713  kmlem8 4752  iscard 4833  iscard2 4834  alephon 4845  ltpiord 4995  subadd 5351  negcon2t 5391  xrlenltt 5481  divmul 5682  divne0bt 5699  dfinfmr 6022  elznn 6105  nn0subt 6116  zmax 6176  zqt 6206  icounlem 6353  snunioolem 6355  ruclem24 7484  iscld4 7646  qdensere 7701  lmbrf 7882  lmclim 7914  metcld 7917  logeftb 8703  h2hcau 8788  ch0psst 9307  h1de2ctlem 9417  hoeqt 9626  adjsymt 9699  dfadj2 9752  nmcopexlem1 9889  nmcfnexlem1 9918  adjbdlnt 9954  mdbr2 10161  mdsl2 10186  elo 10381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain