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

Theorem biimparc 283
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 149 . 2 (χ → (φψ))
32imp 115 1 ((χ φ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  biantr  858  elrab3t  2691  difprsnss  3493  elpw2g  3901  elon2  4079  ideqg  4430  elrnmpt1s  4527  elrnmptg  4529  fun11iun  5090  eqfnfv2  5209  fmpt  5262  elunirn  5348  tposfo2  5823  tposf12  5825  dom2lem  6188  enfii  6253  ltexprlemm  6574  elreal2  6728
  Copyright terms: Public domain W3C validator