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

Theorem syl5rbbr 188
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 127 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 186 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:  xordc  1299  sbal2  1914  eqsnm  3554  fnressn  5377  fressnfv  5378  eluniimadm  5432  genpassl  6680  genpassu  6681  1idprl  6746  1idpru  6747  axcaucvglemres  7031  negeq0  7328  muleqadd  7723  crap0  7986  addltmul  8218  fzrev  9048  modq0  9279  cjap0  9735  cjne0  9736  caucvgrelemrec  9806  lenegsq  9922  dvdsabseq  10159  elabgf0  10303
  Copyright terms: Public domain W3C validator