MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimparc Structured version   Unicode version

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

Proof of Theorem biimparc
StepHypRef Expression
1 biimpa.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprcd 228 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 430 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  biantr  939  elrab3t  3227  difprsnss  4135  elpw2g  4587  ideqg  5005  elrnmpt1s  5101  elrnmptg  5103  elon2  5453  eqfnfv2  5992  fmpt  6058  elunirn  6171  fun11iun  6767  tposfo2  7007  tposf12  7009  dom2lem  7619  enfii  7798  ssnnfi  7800  ac6sfi  7824  unfilem1  7844  inf3lem2  8143  infdiffi  8171  dfac5lem5  8565  dfac2  8568  dfac12k  8584  cfslb2n  8705  enfin2i  8758  fin23lem19  8773  axdc2lem  8885  axdc3lem4  8890  winainflem  9125  indpi  9339  ltexnq  9407  ltbtwnnq  9410  ltexprlem6  9473  prlem936  9479  elreal2  9563  fimaxre3  10560  expnbnd  12407  opfi1uzind  12658  repswswrd  12889  climcnds  13908  fprod2dlem  14033  fprodle  14049  unbenlem  14851  acsfn  15564  lsmcv  18363  maducoeval2  19663  bastop2  20008  neipeltop  20143  rnelfmlem  20965  isfcls  21022  tgphaus  21129  mbfi1fseqlem4  22674  ulm2  23338  ax5seglem5  24961  wlkdvspthlem  25335  wlknwwlknsur  25438  spanunsni  27230  nonbooli  27302  nmopun  27665  lncnopbd  27688  pjnmopi  27799  sumdmdlem  28069  spc2ed  28104  disjun0  28207  rnmpt2ss  28278  esumpcvgval  28907  bnj545  29714  bnj900  29748  bnj1498  29878  soseq  30499  btwnconn1lem7  30865  ivthALT  30996  topfneec  31016  bj-snglss  31532  mptsnunlem  31704  icoreresf  31719  poimirlem14  31918  poimirlem22  31926  poimirlem26  31930  poimirlem29  31933  ovoliunnfl  31946  voliunnfl  31948  volsupnfl  31949  fdc  32038  ismtyres  32104  isdrngo3  32162  lshpset2N  32654  3dimlem1  32992  3dim3  33003  cdleme31fv2  33929  isnumbasgrplem3  35934  pm13.13b  36729  ax6e2ndeqALT  37301  sineq0ALT  37307  elrnmpt1sf  37425  usgrop  39044  egrsubgr  39122  nn0sumshdiglemB  40052
  Copyright terms: Public domain W3C validator