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

Theorem bitr2id 192
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr2id.1 (𝜑𝜓)
bitr2id.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
bitr2id (𝜒 → (𝜃𝜑))

Proof of Theorem bitr2id
StepHypRef Expression
1 bitr2id.1 . . 3 (𝜑𝜓)
2 bitr2id.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:  bitr3di  194  pm5.17dc  899  dn1dc  955  csbabg  3110  uniiunlem  3236  inimasn  5026  cnvpom  5151  fnresdisj  5306  f1oiso  5802  reldm  6162  mptelixpg  6708  1idprl  7539  1idpru  7540  nndiv  8906  fzn  9985  fz1sbc  10039  metrest  13221
  Copyright terms: Public domain W3C validator