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

Theorem biimpar 291
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 156 . 2 (𝜑 → (𝜒𝜓))
32imp 122 1 ((𝜑𝜒) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  exbiri  374  bitr  456  eqtr  2105  opabss  3894  euotd  4072  wetriext  4382  sosng  4499  xpsspw  4538  brcogw  4593  funimaexglem  5083  funfni  5100  fnco  5108  fnssres  5113  fn0  5119  fnimadisj  5120  fnimaeq0  5121  foco  5227  foimacnv  5255  fvelimab  5344  fvopab3ig  5362  dff3im  5428  dffo4  5431  fmptco  5448  f1eqcocnv  5552  f1ocnv2d  5830  fnexALT  5866  xp1st  5918  xp2nd  5919  tfrlemiubacc  6077  tfri2d  6083  tfr1onlemubacc  6093  tfrcllemubacc  6106  tfri3  6114  ecelqsg  6325  elqsn0m  6340  fidifsnen  6566  recclnq  6930  nq0a0  6995  qreccl  9096  difelfzle  9510  exfzdc  9616  modifeq2int  9758  frec2uzlt2d  9776  1elfz0hash  10179  caucvgrelemcau  10378  recvalap  10495  fzomaxdiflem  10510  fsumparts  10827  divconjdvds  10932  ndvdssub  11012  zsupcllemstep  11023  rplpwr  11098  dvdssqlem  11101  eucialgcvga  11122  mulgcddvds  11158  isprm2lem  11180
  Copyright terms: Public domain W3C validator