MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5rbb Unicode version

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
StepHypRef Expression
1 syl5rbb.1 . . 3
2 syl5rbb.2 . . 3
31, 2syl5bb 257 . 2
43bicomd 201 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator