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  936  elrab3t  2839  difprsnss  3658  elpw2g  4081  elon2  4298  ideqg  4690  elrnmpt1s  4789  elrnmptg  4791  fun11iun  5388  eqfnfv2  5519  fmpt  5570  elunirn  5667  spc2ed  6130  tposfo2  6164  tposf12  6166  dom2lem  6666  enfii  6768  ac6sfi  6792  ltexprlemm  7415  elreal2  7645  fihasheqf1oi  10541  bastop2  12263
  Copyright terms: Public domain W3C validator