Theorem syl6bbr 416

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

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

Proof of Theorem syl6bbr

Step	Hyp	Ref	Expression
1		syl6bbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bbr.2	. . 3 |- (th <-> ch)
3	2	bicomi 150	. 2 |- (ch <-> th)
4	1, 3	syl6bb 414	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  3bitr4g 428  biorf 551  19.17 731  eueq3 1430  r19.3rzv 1767  r19.9rzv 1768  otthg 1900  copsexg 1902  reuuni1 1955  iununi 2037  sotrieq 2149  ordelpss 2226  ordsucun 2333  dfom2 2374  peano5 2394  brinxp 2466  fcnvres 2768  fnopabfv 2858  fniunfv 2860  fvreseq 2882  ordgt0ge1 3114  pw2en 3348  mapenlem2 3385  mapxpen 3390  r1pw 3529  rankonid 3538  aceq5lem4 3561  cardalephex 3691  indpi 3828  ltmpq 3871  distrlem5pr 3925  prlem934b 3932  suplem2pr 3956  letri3t 4283  halfpost 4508  zrevaddclt 4592  elnnnn0 4594  indstr 4611  qrevaddclt 4648  om2uzf1o 4656  seqlem2 4663  lt2sqe 4700  le2sqe 4701  znnen 4930  ocsh 5164  shle0t 5367  jplem2 5702  cvbr2t 5715  chrelat3t 5762

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