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

Theorem biimpar 285
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 151 . 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:  exbiri  368  bitr  449  eqtr  2073  opabss  3848  euotd  4018  wetriext  4328  sosng  4440  xpsspw  4477  brcogw  4531  funimaexglem  5009  funfni  5026  fnco  5034  fnssres  5039  fn0  5045  fnimadisj  5046  fnimaeq0  5047  foco  5143  foimacnv  5171  fvelimab  5256  fvopab3ig  5273  dff3im  5339  dffo4  5342  fmptco  5357  f1eqcocnv  5458  f1ocnv2d  5731  fnexALT  5767  xp1st  5819  xp2nd  5820  tfrlemiubacc  5974  tfri2d  5980  tfri3  5983  ecelqsg  6189  elqsn0m  6204  fidifsnen  6361  recclnq  6547  nq0a0  6612  qreccl  8673  difelfzle  9093  modifeq2int  9330  frec2uzlt2d  9348  caucvgrelemcau  9800  recvalap  9916  fzomaxdiflem  9931  divconjdvds  10153
  Copyright terms: Public domain W3C validator