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

Theorem biimparc 293
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 158 . 2 (𝜒 → (𝜑𝜓))
32imp 122 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  biantr  898  elrab3t  2770  difprsnss  3575  elpw2g  3992  elon2  4203  ideqg  4587  elrnmpt1s  4685  elrnmptg  4687  fun11iun  5274  eqfnfv2  5398  fmpt  5449  elunirn  5545  spc2ed  5998  tposfo2  6032  tposf12  6034  dom2lem  6489  enfii  6590  ac6sfi  6614  ltexprlemm  7159  elreal2  7368  fihasheqf1oi  10196
  Copyright terms: Public domain W3C validator