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  2033  opabss  3787  euotd  3957  sosng  4331  xpsspw  4368  brcogw  4422  funimaexglem  4899  funfni  4916  fnco  4924  fnssres  4929  fn0  4935  fnimadisj  4936  fnimaeq0  4937  foco  5032  foimacnv  5060  fvelimab  5145  fvopab3ig  5162  dff3im  5228  dffo4  5231  fmptco  5246  f1eqcocnv  5347  f1ocnv2d  5618  fnexALT  5654  xp1st  5706  xp2nd  5707  tfrlemiubacc  5856  tfri2d  5863  tfri3  5866  ecelqsg  6061  elqsn0m  6076  recclnq  6240  nq0a0  6301  qreccl  8061
  Copyright terms: Public domain W3C validator