Theorem syl5bbr 534

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

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

This theorem is referenced by:  3bitr3g 554  19.16 1048  19.19 1055  sbco2 1255  necon1bbid 1619  necon4abid 1629  elabf 1896  sbceq1a 1944  opabsb 2815  iunpw 2914  ordunisuc2 3115  dfom2 3133  tfinds 3161  xp11 3476  fneu 3592  fnssresb 3599  dmfco 3773  fvco 3774  dffo4 3820  elunirn 3868  oaabs 4252  brecop 4306  zorn2lem7 4794  card1 4833  alephval2 4902  ltpiord 5015  map2psrpr 5220  suppsr 5222  supsrlem6 5230  supre 5260  mul0or 5694  lt2msq 5881  infm3 6054  infmsup 6068  supxrbnd1 6095  supxrbnd2 6096  uzindOLD 6208  iccnegt 6407  eluzt 6426  sqr00t 6714  geoisum1c 7245  reeff1o 7426  bcthlem9 8007  sincosq3sgn 8706  sincosq4sgn 8707  efifolem6 8727  pjthlem11 9229  ch0psst 9369  jplem1 10195  hatomistic 10289  cdjreu 10359  ghomf1olem 10396  elo 10444  hgrablkcard 10774

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