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

Theorem syl5rbb 273
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 272 . 2 (𝜒 → (𝜑𝜃))
43bicomd 213 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  syl5rbbr  275  necon1abid  2970  necon4abid  2972  uniiunlem  3833  r19.9rzv  4209  inimasn  5708  fnresdisj  6162  f1oiso  6764  reldm  7386  rdglim2  7697  mptelixpg  8111  1idpr  10043  nndiv  11253  fz1sbc  12609  grpid  17658  znleval  20105  fbunfip  21874  lmflf  22010  metcld2  23305  lgsne0  25259  isuvtx  26497  isuvtxaOLD  26498  loopclwwlkn1b  27171  clwwlknun  27261  clwwlknunOLD  27265  frgrncvvdeqlem2  27454  isph  27986  ofpreima  29774  eulerpartlemd  30737  bnj168  31105  opelco3  31983  wl-2sb6d  33654  poimirlem26  33748  cnambfre  33771  heibor1  33922  opltn0  34980  cvrnbtwn2  35065  cvrnbtwn4  35069  atlltn0  35096  pmapjat1  35642  dih1dimatlem  37120  2rexfrabdioph  37862  dnwech  38120  rfovcnvf1od  38800  uneqsn  38823  csbabgOLD  39552  2reu4a  41695  lighneallem2  42033  isrnghm  42402  rnghmval2  42405
  Copyright terms: Public domain W3C validator