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

Theorem syl5rbbr 194
 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 131 . 2 (𝜑𝜓)
3 syl5rbbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5rbb 192 1 (𝜒 → (𝜃𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  xordc  1329  sbal2  1947  eqsnm  3605  fnressn  5497  fressnfv  5498  eluniimadm  5558  genpassl  7144  genpassu  7145  1idprl  7210  1idpru  7211  axcaucvglemres  7495  negeq0  7797  muleqadd  8198  crap0  8479  addltmul  8713  fzrev  9559  modq0  9797  cjap0  10402  cjne0  10403  caucvgrelemrec  10473  lenegsq  10589  isumss  10844  fsumsplit  10862  sumsplitdc  10887  dvdsabseq  11187  oddennn  11544  elabgf0  11950
 Copyright terms: Public domain W3C validator