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

Theorem syl5rbb 287
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 286 . 2 (𝜒 → (𝜑𝜃))
43bicomd 226 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  bitr3di  289  necon1abid  3025  necon4abid  3027  uniiunlem  4012  r19.9rzv  4403  2reu4lem  4423  inimasn  5980  fnresdisj  6439  f1oiso  7083  reldm  7725  rdglim2  8051  mptelixpg  8482  1idpr  10440  nndiv  11671  fz1sbc  12978  grpid  18131  znleval  20246  fbunfip  22474  lmflf  22610  metcld2  23911  lgsne0  25919  isuvtx  27185  loopclwwlkn1b  27827  clwwlknun  27897  frgrncvvdeqlem2  28085  isph  28605  ofpreima  30428  eulerpartlemd  31734  bnj168  32110  cardpred  32473  opelco3  33131  wl-2sb6d  34959  poimirlem26  35083  cnambfre  35105  heibor1  35248  opltn0  36486  cvrnbtwn2  36571  cvrnbtwn4  36575  atlltn0  36602  pmapjat1  37149  dih1dimatlem  38625  2rexfrabdioph  39735  dnwech  39990  rfovcnvf1od  40703  uneqsn  40724  lighneallem2  44122  isrnghm  44514  rnghmval2  44517
  Copyright terms: Public domain W3C validator