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

Theorem syl5rbb 192
 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 191 . 2 (𝜒 → (𝜑𝜃))
43bicomd 140 1 (𝜒 → (𝜃𝜑))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  syl5rbbr  194  pm5.17dc  889  dn1dc  944  csbabg  3056  uniiunlem  3180  inimasn  4951  cnvpom  5076  fnresdisj  5228  f1oiso  5720  reldm  6077  mptelixpg  6621  1idprl  7391  1idpru  7392  nndiv  8754  fzn  9815  fz1sbc  9869  metrest  12664  bj-indeq  13116
 Copyright terms: Public domain W3C validator