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

Theorem syl5rbb 182
 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 181 . 2 (χ → (φθ))
43bicomd 129 1 (χ → (θφ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  syl5rbbr  184  pm5.17dc  809  dn1dc  866  csbabg  2901  uniiunlem  3022  inimasn  4684  cnvpom  4803  fnresdisj  4952  f1oiso  5408  reldm  5754  1idprl  6565  1idpru  6566  nndiv  7715  fzn  8656  fz1sbc  8708  bj-indeq  9364
 Copyright terms: Public domain W3C validator