ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl5rbb GIF version

Theorem syl5rbb 192
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-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 191 . 2 (𝜒 → (𝜑𝜃))
43bicomd 140 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  syl5rbbr  194  pm5.17dc  874  dn1dc  929  csbabg  3031  uniiunlem  3155  inimasn  4926  cnvpom  5051  fnresdisj  5203  f1oiso  5695  reldm  6052  mptelixpg  6596  1idprl  7366  1idpru  7367  nndiv  8729  fzn  9790  fz1sbc  9844  metrest  12602  bj-indeq  13054
  Copyright terms: Public domain W3C validator