Theorem syl6rbbr 539

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

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

This theorem is referenced by:  baib 685  reu8 1936  sbcgf 1986  sbcel12g 2011  disjssun 2326  r19.28zv 2350  r19.37zv 2351  r19.45zv 2352  r19.27zv 2353  r19.36zv 2354  ralidm 2357  iunconst 2572  elpwun 2911  dfom2 3133  funssres 3552  fncnv 3561  fcoi1 3645  fcoi2 3646  funimass4 3763  dffo3 3819  funfvima 3852  isomin 3899  f1oweALT 3906  tz7.48-2 3957  eloprabg 4007  oe0m1 4160  pw2en 4446  xpmapenlem4 4499  aceq3 4733  kmlem8 4772  iscard 4853  iscard2 4854  alephon 4865  ltpiord 5015  subadd 5371  negcon2t 5411  xrlenltt 5501  divmul 5705  divne0bt 5728  dfinfmr 6067  elznn 6150  nn0subt 6161  zmax 6220  zqt 6260  icounlem 6412  snunioolem 6414  ruclem24 7533  iscld4 7696  qdensere 7751  lmbrf 7930  lmclim 7963  metcld 7967  logeftb 8764  h2hcau 8849  ch0psst 9369  h1de2ctlem 9478  hoeqt 9686  adjsymt 9759  dfadj2 9812  nmcopexlem1 9951  nmcfnexlem1 9980  adjbdlnt 10016  mdbr2 10223  mdsl2 10249  elo 10444

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