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

Theorem biimparc 287
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 153 . 2 (𝜒 → (𝜑𝜓))
32imp 119 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  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:  biantr  870  elrab3t  2720  difprsnss  3530  elpw2g  3938  elon2  4141  ideqg  4515  elrnmpt1s  4612  elrnmptg  4614  fun11iun  5175  eqfnfv2  5294  fmpt  5347  elunirn  5433  spc2ed  5882  tposfo2  5913  tposf12  5915  dom2lem  6283  enfii  6366  ac6sfi  6383  ltexprlemm  6756  elreal2  6965
  Copyright terms: Public domain W3C validator