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

Theorem biimpar 293
Description: Inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
Ref Expression
biimpa.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
biimpar  |-  ( (
ph  /\  ch )  ->  ps )

Proof of Theorem biimpar
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 157 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 123 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 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  2132  opabss  3952  euotd  4136  wetriext  4451  sosng  4572  xpsspw  4611  brcogw  4668  funimaexglem  5164  funfni  5181  fnco  5189  fnssres  5194  fn0  5200  fnimadisj  5201  fnimaeq0  5202  foco  5313  foimacnv  5341  fvelimab  5431  fvopab3ig  5449  dff3im  5519  dffo4  5522  fmptco  5540  f1eqcocnv  5646  f1ocnv2d  5928  fnexALT  5965  xp1st  6017  xp2nd  6018  tfrlemiubacc  6181  tfri2d  6187  tfr1onlemubacc  6197  tfrcllemubacc  6210  tfri3  6218  ecelqsg  6436  elqsn0m  6451  fidifsnen  6717  recclnq  7148  nq0a0  7213  qreccl  9336  difelfzle  9804  exfzdc  9910  modifeq2int  10052  frec2uzlt2d  10070  1elfz0hash  10445  caucvgrelemcau  10644  recvalap  10761  fzomaxdiflem  10776  2zsupmax  10889  fsumparts  11131  divconjdvds  11395  ndvdssub  11475  zsupcllemstep  11486  rplpwr  11561  dvdssqlem  11564  eucalgcvga  11585  mulgcddvds  11621  isprm2lem  11643  uniopn  12011  ntrval  12122  clsval  12123  neival  12155  restdis  12196  lmbrf  12226  cnpnei  12230  dviaddf  12624  dvimulf  12625
  Copyright terms: Public domain W3C validator