Theorem syl6rbbr 541

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 539	1 |- (ph -> (th <-> ps))

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

This theorem is referenced by:  baib 687  reu8 1939  sbcgf 1989  sbcel12g 2014  disjssun 2330  r19.28zv 2354  r19.37zv 2355  r19.45zv 2356  r19.27zv 2357  r19.36zv 2358  ralidm 2361  iunconst 2576  elpwun 2917  dfom2 3139  funssres 3558  fncnv 3567  fcoi1 3651  fcoi2 3652  funimass4 3769  dffo3 3825  funfvima 3858  isomin 3905  f1oweALT 3912  tz7.48-2 3963  eloprabg 4013  oe0m1 4166  pw2en 4452  xpmapenlem4 4505  aceq3 4743  kmlem8 4782  iscard 4864  iscard2 4865  alephon 4876  ltpiord 5027  subadd 5383  negcon2t 5423  xrlenltt 5513  divmul 5717  divne0bt 5735  dfinfmr 6069  elznn 6152  nn0subt 6163  zmax 6222  zqt 6261  icounlem 6413  snunioolem 6415  ruclem24 7534  iscld4 7693  qdensere 7748  lmbrf 7927  lmclim 7960  metcld 7964  logeftb 8759  h2hcau 8844  ch0psst 9364  h1de2ctlem 9473  hoeqt 9681  adjsymt 9754  dfadj2 9807  nmcopexlem1 9946  nmcfnexlem1 9975  adjbdlnt 10011  mdbr2 10218  mdsl2 10244  elo 10439

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