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

Theorem biimparc 297
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 159 . 2 (𝜒 → (𝜑𝜓))
32imp 123 1 ((𝜒𝜑) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  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:  biantr  921  elrab3t  2812  difprsnss  3628  elpw2g  4051  elon2  4268  ideqg  4660  elrnmpt1s  4759  elrnmptg  4761  fun11iun  5356  eqfnfv2  5487  fmpt  5538  elunirn  5635  spc2ed  6098  tposfo2  6132  tposf12  6134  dom2lem  6634  enfii  6736  ac6sfi  6760  ltexprlemm  7376  elreal2  7606  fihasheqf1oi  10502  bastop2  12180
  Copyright terms: Public domain W3C validator