Theorem syl5rbb 258

Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.)

Hypotheses

Ref	Expression
syl5rbb.1
syl5rbb.2

Assertion

Ref	Expression
syl5rbb

Proof of Theorem syl5rbb

Step	Hyp	Ref	Expression
1		syl5rbb.1	. . 3
2		syl5rbb.2	. . 3
3	1, 2	syl5bb 257	. 2
4	3	bicomd 201	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  syl5rbbr  260  necon1abid  2705  necon4abid  2708  uniiunlem  3587  csbabgOLD  3856  inimasn  5428  fnresdisj  5696  f1oiso  6247  reldm  6851  rdglim2  7117  mptelixpg  7526  1idpr  9428  nndiv  10601  fz1sbc  11783  grpid  16085  znleval  18593  fbunfip  20370  lmflf  20506  metcld2  21745  lgsne0  23608  isph  25737  ofpreima  27507  eulerpartlemd  28305  opelco3  29208  wl-2sb6d  30008  cnambfre  30063  heibor1  30306  2rexfrabdioph  30729  dnwech  30994  2reu4a  32194  isrnghm  32698  rnghmval2  32701  bnj168  33785  opltn0  34915  cvrnbtwn2  35000  cvrnbtwn4  35004  atlltn0  35031  pmapjat1  35577  dih1dimatlem  37056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185