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

Theorem ibir 176
 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 140 . 2 (𝜑 → (𝜑𝜓))
32ibi 175 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:  pm5.21nii  694  elpr2  3582  eusv2i  4413  ffdm  5337  ov  5934  ovg  5953  nnacl  6420  elpm2r  6604  ltnqpri  7497  ltxrlt  7926  uzaddcl  9480  expcllem  10412  qexpclz  10422  1exp  10430  facnn  10583  fac0  10584  fac1  10585  bcn2  10620  znnen  12099
 Copyright terms: Public domain W3C validator