Theorem syl6rbbr 542

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

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

This theorem is referenced by:  baib 689  reu8 1982  sbcgf 2034  sbcel12g 2062  disjssun 2379  r19.28zv 2404  r19.37zv 2405  r19.45zv 2406  r19.27zv 2407  r19.36zv 2408  ralidm 2411  ralsng 2489  iunconst 2640  elpwun 3134  dfom2 3220  funssres 3657  fncnv 3666  fcoi1 3752  fcoi2 3753  funimass4 3874  dffo3 3933  funfvima 3966  isomin 4013  f1oweALT 4020  eloprabg 4067  tz7.48-2 4258  oe0m1 4296  pw2en 4587  xpmapenlem4 4646  aceq3 4879  kmlem8 4918  iscard 5003  iscard2 5004  alephon 5015  ltpiord 5169  subaddi 5525  negcon2 5565  xrlenlt 5655  divmuli 5857  divne0b 5874  dfinfmr 6235  elznn 6318  nn0sub 6329  zmax 6392  zq 6399  icounlem 6539  snunioolem 6541  ruclem24 7745  iscld4 7906  qdensere 7961  lmbrf 8141  lmclim 8174  metcld 8178  sinq34lt0t 8976  logeftb 9036  h2hcau 9124  ch0pss 9645  h1de2ctlem 9754  adjsym 10039  dfadj2 10092  nmcopexlem1 10230  nmcfnexlem1 10259  adjbdln 10295  mdbr2 10504  mdsl2i 10530  elo 10733  topbasfne 11560  neifg 11644  opabex3 11806  heiborlem23 12033  heiborlem29 12039

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 145  df-an 223

Copyright terms: Public domain