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

Theorem syl6rbb 196
 Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6rbb.1 (𝜑 → (𝜓𝜒))
syl6rbb.2 (𝜒𝜃)
Assertion
Ref Expression
syl6rbb (𝜑 → (𝜃𝜓))

Proof of Theorem syl6rbb
StepHypRef Expression
1 syl6rbb.1 . . 3 (𝜑 → (𝜓𝜒))
2 syl6rbb.2 . . 3 (𝜒𝜃)
31, 2syl6bb 195 . 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:  syl6rbbr  198  bibif  687  pm5.61  783  oranabs  804  pm5.7dc  938  nbbndc  1372  resopab2  4866  xpcom  5085  f1od2  6132  map1  6706  ac6sfi  6792  elznn0  9069  rexuz3  10762  xrmaxiflemcom  11018  metrest  12675  sincosq3sgn  12909  sincosq4sgn  12910
 Copyright terms: Public domain W3C validator