Theorem syl5bbr 593

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

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

This theorem is referenced by:  3bitr3g 613  19.16 1395  19.19 1402  sbco2 1629  necon1bbid 2062  necon4abid 2077  elabgt 2400  elabf 2402  cbvab 2419  sbceq1a 2456  opelopabsbOLD 3565  dffr2 3627  iunpw 3858  ordunisuc2 3926  tfinds 3942  tfindsOLD 3943  dfom2 3951  opelxpex2 4119  xp11 4347  fneuOLD 4518  fnssresb 4525  dmfco 4735  fvco 4736  dffo4 4793  elunirn 4844  dfoprab4s 5056  1stconst 5070  2ndconst 5071  oaabs 5309  brecop 5365  zorn2lem7 5956  card1 5983  alephval2 6050  ltpiord 6167  map2psrpr 6372  suppsr 6374  supsrlem6 6382  supre 6412  mul0ori 6882  lt2msqi 7064  infm3 7263  infmsup 7277  supxrbnd1 7304  supxrbnd2 7305  uzindOLD 7420  iccneg 7576  eluz 7595  sqr00 7964  geoisum1c 8507  reeff1o 8691  absefib 8750  efieq1re 8751  bcthlem9 9285  sincosq3sgn 10055  sincosq4sgn 10056  efifolem6 10081  pjthlem11 10862  ch0pss 11002  jplem1 11840  hatomistici 11934  mdsymlem5 11979  cdjreui 12004  bnj100 12449  bnj99 12450  bnj137 12469  ghomf1olem 13637  divalglem4 13699  divalgmod 13709  isprm3 13776  brtxp 14067  dfoprab4spop 14339  elo 14342  bwt2 14960  lvsovso2 15039  supnuf 15041  supexr 15043  alexsub 15441  resoprab2 15710  sdc 15811  fdc 15812  fsumltisum 15824  fsumleisum 15827  pcoval 16073  0nelqs2 16269  prter3 16286  hgrablkcard 16296  fveqsb 16431  strdif 16719  glb0 16920

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 164  df-an 242

Copyright terms: Public domain