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

Theorem bitr2id 193
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, 2bitrid 192 . 2 (𝜒 → (𝜑𝜃))
43bicomd 141 1 (𝜒 → (𝜃𝜑))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  bitr3di  195  pm5.17dc  904  dn1dc  960  csbabg  3118  uniiunlem  3244  inimasn  5046  cnvpom  5171  fnresdisj  5326  f1oiso  5826  reldm  6186  mptelixpg  6733  1idprl  7588  1idpru  7589  nndiv  8959  fzn  10041  fz1sbc  10095  grpid  12911  metrest  13976
  Copyright terms: Public domain W3C validator