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

Theorem biimparc 299
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimparc ((𝜒𝜑) → 𝜓)

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimprcd 160 . 2 (𝜒 → (𝜑𝜓))
32imp 124 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  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:  biantr  954  elrab3t  2907  difprsnss  3745  elpw2g  4174  elon2  4394  ideqg  4796  elrnmpt1s  4895  elrnmptg  4897  fun11iun  5501  eqfnfv2  5635  fmpt  5687  elunirn  5788  spc2ed  6259  tposfo2  6293  tposf12  6295  dom2lem  6799  enfii  6903  ac6sfi  6927  ltexprlemm  7630  elreal2  7860  fihasheqf1oi  10802  fprod2dlemstep  11665  bastop2  14061
  Copyright terms: Public domain W3C validator