Theorem syl5bbr 533

Description: A syllogism inference from two biconditionals.

Hypotheses

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

Assertion

Ref	Expression
syl5bbr	|- (ph -> (th <-> ch))

Proof of Theorem syl5bbr

Step	Hyp	Ref	Expression
1		syl5bbr.1	. 2 |- (ph -> (ps <-> ch))
2		syl5bbr.2	. . 3 |- (ps <-> th)
3	2	bicomi 172	. 2 |- (th <-> ps)
4	1, 3	syl5bb 531	1 |- (ph -> (th <-> ch))

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

This theorem is referenced by:  3bitr3g 553  19.16 1046  19.19 1053  sbco2 1253  necon1bbid 1616  necon4abid 1626  elabf 1892  sbceq1a 1940  opabsb 2810  iunpw 2909  ordunisuc2 3110  dfom2 3128  tfinds 3156  xp11 3468  fneu 3584  fnssresb 3591  dmfco 3764  fvco 3765  dffo4 3811  elunirn 3859  oaabs 4242  brecop 4296  zorn2lem7 4774  card1 4813  alephval2 4882  ltpiord 4995  map2psrpr 5200  suppsr 5202  supsrlem6 5210  supre 5240  ltnetOLD 5497  mul0or 5671  lt2msq 5837  infm3 6009  infmsup 6023  supxrbnd1 6050  supxrbnd2 6051  uzindOLD 6164  ioonegt 6347  iccnegt 6348  eluzt 6366  sqr00t 6652  geoisum1c 7188  reeff1o 7376  bcthlem9 7957  sincosq3sgn 8642  sincosq4sgn 8643  efifolem6 8661  pjthlem11 9167  ch0psst 9307  jplem1 10133  hatomistic 10226  cdjreu 10293  ghomf1olem 10330  elo 10381  hgrablkcard 10646

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