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

Theorem ibir 170
Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
ibir.1 (𝜑 → (𝜓𝜑))
Assertion
Ref Expression
ibir (𝜑𝜓)

Proof of Theorem ibir
StepHypRef Expression
1 ibir.1 . . 3 (𝜑 → (𝜓𝜑))
21bicomd 133 . 2 (𝜑 → (𝜑𝜓))
32ibi 169 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:  pm5.21nii  630  elpr2  3425  eusv2i  4215  ffdm  5089  ov  5648  ovg  5667  nnacl  6090  ltnqpri  6750  ltxrlt  7144  uzaddcl  8625  expcllem  9431  qexpclz  9441  1exp  9449  facnn  9595  fac0  9596  fac1  9597  bcn2  9632
  Copyright terms: Public domain W3C validator