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

Theorem syl5rbbr 193
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 130 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 191 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  xordc  1328  sbal2  1946  eqsnm  3599  fnressn  5483  fressnfv  5484  eluniimadm  5544  genpassl  7081  genpassu  7082  1idprl  7147  1idpru  7148  axcaucvglemres  7432  negeq0  7734  muleqadd  8135  crap0  8416  addltmul  8650  fzrev  9494  modq0  9732  cjap0  10337  cjne0  10338  caucvgrelemrec  10408  lenegsq  10524  isumss  10779  fsumsplit  10797  sumsplitdc  10822  dvdsabseq  11122  oddennn  11479  elabgf0  11632
  Copyright terms: Public domain W3C validator