Theorem syl5bbr 537

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

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

This theorem is referenced by:  3bitr3g 557  19.16 1084  19.19 1091  sbco2 1293  necon1bbid 1663  necon4abid 1673  elabf 1942  sbceq1a 1989  opelopabsb 2892  iunpw 3137  ordunisuc2 3198  tfinds 3212  dfom2 3220  xp11 3561  fneu 3698  fnssresb 3705  dmfco 3884  fvco 3885  dffo4 3934  elunirn 3982  dfoprab4s 4176  1stconst 4190  2ndconst 4191  oaabs 4392  brecop 4447  zorn2lem7 4940  card1 4981  alephval2 5052  ltpiord 5169  map2psrpr 5374  suppsr 5376  supsrlem6 5384  supre 5414  mul0ori 5846  lt2msqi 6026  infm3 6222  infmsup 6236  supxrbnd1 6263  supxrbnd2 6264  uzindOLD 6379  iccneg 6534  eluz 6553  sqr00 6915  geoisum1c 7450  reeff1o 7634  absefib 7693  efieq1re 7694  bcthlem9 8218  sincosq3sgn 8973  sincosq4sgn 8974  efifolem6 8999  pjthlem11 9505  ch0pss 9645  jplem1 10476  hatomistici 10570  cdjreui 10641  ghomf1olem 10681  elo 10733  bwt2 11123  alexsub 11500  resoprab2 11809  sdc 11877  fsumltisum 11887  fsumleisum 11890  hgrablkcard 12200

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