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