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

Theorem biimpar 297
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 158 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
32imp 124 1  |-  ( (
ph  /\  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  exbiri  382  bitr  472  eqtr  2195  opabss  4064  euotd  4251  wetriext  4573  sosng  4696  xpsspw  4735  brcogw  4792  funimaexglem  5295  funfni  5312  fnco  5320  fnssres  5325  fn0  5331  fnimadisj  5332  fnimaeq0  5333  foco  5444  foimacnv  5475  fvelimab  5568  fvopab3ig  5586  dff3im  5657  dffo4  5660  fmptco  5678  f1eqcocnv  5786  f1ocnv2d  6069  fnexALT  6106  xp1st  6160  xp2nd  6161  tfrlemiubacc  6325  tfri2d  6331  tfr1onlemubacc  6341  tfrcllemubacc  6354  tfri3  6362  ecelqsg  6582  elqsn0m  6597  fidifsnen  6864  recclnq  7379  nq0a0  7444  qreccl  9628  difelfzle  10117  exfzdc  10223  modifeq2int  10369  frec2uzlt2d  10387  1elfz0hash  10767  caucvgrelemcau  10970  recvalap  11087  fzomaxdiflem  11102  2zsupmax  11215  2zinfmin  11232  fsumparts  11459  ntrivcvgap  11537  divconjdvds  11835  ndvdssub  11915  zsupcllemstep  11926  rplpwr  12008  dvdssqlem  12011  eucalgcvga  12038  mulgcddvds  12074  isprm2lem  12096  powm2modprm  12232  coprimeprodsq  12237  pythagtriplem11  12254  pythagtriplem13  12256  grpidd  12691  ismndd  12727  mulgaddcom  12892  isringd  13043  uniopn  13159  ntrval  13270  clsval  13271  neival  13303  restdis  13344  lmbrf  13375  cnpnei  13379  dviaddf  13829  dvimulf  13830  logbgt0b  14044  lgslem4  14064  lgsmod  14087  lgsdir2lem2  14090  lgsdir2  14094  lgsne0  14099  lgsmulsqcoprm  14107  2sqlem4  14114
  Copyright terms: Public domain W3C validator