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

Theorem syl5rbb 186
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 185 . 2 (𝜒 → (𝜑𝜃))
43bicomd 133 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  syl5rbbr  188  pm5.17dc  821  dn1dc  878  csbabg  2934  uniiunlem  3055  inimasn  4768  cnvpom  4887  fnresdisj  5036  f1oiso  5492  reldm  5839  1idprl  6745  1idpru  6746  nndiv  8029  fzn  9007  fz1sbc  9059  bj-indeq  10419
  Copyright terms: Public domain W3C validator