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

Theorem biimpar 281
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1 (φ → (ψχ))
Assertion
Ref Expression
biimpar ((φ χ) → ψ)

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3 (φ → (ψχ))
21biimprd 147 . 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:  exbiri  364  bitr  441  eqtr  2054  opabss  3812  euotd  3982  sosng  4356  xpsspw  4393  brcogw  4447  funimaexglem  4925  funfni  4942  fnco  4950  fnssres  4955  fn0  4961  fnimadisj  4962  fnimaeq0  4963  foco  5059  foimacnv  5087  fvelimab  5172  fvopab3ig  5189  dff3im  5255  dffo4  5258  fmptco  5273  f1eqcocnv  5374  f1ocnv2d  5646  fnexALT  5682  xp1st  5734  xp2nd  5735  tfrlemiubacc  5885  tfri2d  5891  tfri3  5894  ecelqsg  6095  elqsn0m  6110  recclnq  6376  nq0a0  6440  qreccl  8351  difelfzle  8762  frec2uzlt2d  8871
  Copyright terms: Public domain W3C validator