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

Theorem biimpac 286
 Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
biimpac ((𝜓𝜑) → 𝜒)

Proof of Theorem biimpac
StepHypRef Expression
1 biimpa.1 . . 3 (𝜑 → (𝜓𝜒))
21biimpcd 152 . 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 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  gencbvex2  2618  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  ordsuc  4315  onsucuni2  4316  poltletr  4753  tz6.12-1  5228  nfunsn  5235  nnaordex  6131  th3qlem1  6239  ssfiexmid  6367  diffitest  6375  nqnq0pi  6594  distrlem1prl  6738  distrlem1pru  6739  eqle  7168  flodddiv4  10246
 Copyright terms: Public domain W3C validator