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

Theorem syl5rbbr 184
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.)
Hypotheses
Ref Expression
syl5rbbr.1 (ψφ)
syl5rbbr.2 (χ → (ψθ))
Assertion
Ref Expression
syl5rbbr (χ → (θφ))

Proof of Theorem syl5rbbr
StepHypRef Expression
1 syl5rbbr.1 . . 3 (ψφ)
21bicomi 123 . 2 (φψ)
3 syl5rbbr.2 . 2 (χ → (ψθ))
42, 3syl5rbb 182 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:  xordc  1280  sbal2  1895  eqsnm  3516  fnressn  5290  fressnfv  5291  eluniimadm  5345  genpassl  6500  genpassu  6501  1idprl  6556  1idpru  6557  negeq0  7013  muleqadd  7383  crap0  7642  addltmul  7888  fzrev  8662  elabgf0  8850
  Copyright terms: Public domain W3C validator