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  444  eqtr  2039  opabss  3795  euotd  3965  sosng  4340  xpsspw  4377  brcogw  4431  funimaexglem  4908  funfni  4925  fnco  4933  fnssres  4938  fn0  4944  fnimadisj  4945  fnimaeq0  4946  foco  5041  foimacnv  5069  fvelimab  5154  fvopab3ig  5171  dff3im  5237  dffo4  5240  fmptco  5255  f1eqcocnv  5356  f1ocnv2d  5627  fnexALT  5663  xp1st  5715  xp2nd  5716  tfrlemiubacc  5865  tfri2d  5872  tfri3  5875  ecelqsg  6070  elqsn0m  6085  recclnq  6251  nq0a0  6312
  Copyright terms: Public domain W3C validator