Theorem syl5bbr 536

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 534	1 |- (ph -> (th <-> ch))

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

This theorem is referenced by:  3bitr3g 556  19.16 1050  19.19 1057  sbco2 1257  necon1bbid 1622  necon4abid 1632  elabf 1899  sbceq1a 1947  opabsb 2821  iunpw 2920  ordunisuc2 3121  dfom2 3139  tfinds 3167  xp11 3482  fneu 3598  fnssresb 3605  dmfco 3779  fvco 3780  dffo4 3826  elunirn 3874  oaabs 4258  brecop 4312  zorn2lem7 4804  card1 4843  alephval2 4913  ltpiord 5027  map2psrpr 5232  suppsr 5234  supsrlem6 5242  supre 5272  mul0or 5706  lt2msq 5883  infm3 6056  infmsup 6070  supxrbnd1 6097  supxrbnd2 6098  uzindOLD 6210  iccnegt 6408  eluzt 6427  sqr00t 6715  geoisum1c 7245  reeff1o 7426  bcthlem9 8004  sincosq3sgn 8701  sincosq4sgn 8702  efifolem6 8722  pjthlem11 9224  ch0psst 9364  jplem1 10190  hatomistic 10284  cdjreu 10354  ghomf1olem 10391  elo 10439  hgrablkcard 10745

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