Theorem syl6rbbr 417

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 150	. 2 |- (ch <-> th)
4	1, 3	syl6rbb 415	1 |- (ph -> (th <-> ps))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  baib 506  sbcgf 1469  r19.28zv 1769  r19.45zv 1770  r19.27zv 1771  ralidm 1774  raaan 1775  iunconst 2000  dfom2 2374  funssres 2698  fcoi1 2765  fcoi2 2766  funfvima 2904  isomin 2937  f1oweOLD 2944  tz7.48-2 2995  eloprabg 3035  pw2en 3348  xpmapenlem4 3394  aceq3 3556  kmlem13 3592  iscard 3659  iscard2 3660  alephon 3671  ltpiord 3809  subadd 4143  negcon2t 4168  divmul 4218  divneq0bt 4230  leltt 4278  nn0subt 4587  zmax 4618  zqt 4632  ruclem24 4908  ch0psst 5370  h1de2ctlem 5460  mdbr2 5728

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

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org