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

Theorem biimpar 293
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 157 . 2 (𝜑 → (𝜒𝜓))
32imp 123 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  exbiri  377  bitr  461  eqtr  2133  opabss  3960  euotd  4144  wetriext  4459  sosng  4580  xpsspw  4619  brcogw  4676  funimaexglem  5174  funfni  5191  fnco  5199  fnssres  5204  fn0  5210  fnimadisj  5211  fnimaeq0  5212  foco  5323  foimacnv  5351  fvelimab  5443  fvopab3ig  5461  dff3im  5531  dffo4  5534  fmptco  5552  f1eqcocnv  5658  f1ocnv2d  5940  fnexALT  5977  xp1st  6029  xp2nd  6030  tfrlemiubacc  6193  tfri2d  6199  tfr1onlemubacc  6209  tfrcllemubacc  6222  tfri3  6230  ecelqsg  6448  elqsn0m  6463  fidifsnen  6730  recclnq  7164  nq0a0  7229  qreccl  9386  difelfzle  9862  exfzdc  9968  modifeq2int  10110  frec2uzlt2d  10128  1elfz0hash  10503  caucvgrelemcau  10703  recvalap  10820  fzomaxdiflem  10835  2zsupmax  10948  fsumparts  11190  divconjdvds  11454  ndvdssub  11534  zsupcllemstep  11545  rplpwr  11622  dvdssqlem  11625  eucalgcvga  11646  mulgcddvds  11682  isprm2lem  11704  uniopn  12074  ntrval  12185  clsval  12186  neival  12218  restdis  12259  lmbrf  12290  cnpnei  12294  dviaddf  12744  dvimulf  12745
  Copyright terms: Public domain W3C validator