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

Theorem biimparc 473
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 216 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 418 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358
This theorem is referenced by:  biantr  897  difprsnss  3790  elpw2g  4211  elon2  4440  ideqg  4872  elrnmpt1s  4964  elrnmptg  4966  fun11iun  5531  eqfnfv2  5661  fmpt  5719  elunirnALT  5821  tposfo2  6299  tposf12  6301  dom2lem  6944  enfii  7123  ssnnfi  7125  ac6sfi  7146  unfilem1  7166  inf3lem2  7375  infdiffi  7403  dfac5lem5  7799  dfac2  7802  dfac12k  7818  cfslb2n  7939  enfin2i  7992  fin23lem19  8007  axdc2lem  8119  axdc3lem4  8124  winainflem  8360  gruiun  8466  indpi  8576  ltexnq  8644  ltbtwnnq  8647  ltexprlem6  8710  prlem936  8716  elreal2  8799  fimaxre3  9748  expnbnd  11277  climcnds  12357  unbenlem  13002  acsfn  13610  lsmcv  15943  bastop2  16788  rnelfmlem  17699  isfcls  17756  tgphaus  17851  mbfi1fseqlem4  19126  ulm2  19817  spanunsni  22213  nonbooli  22285  nmopun  22649  lncnopbd  22672  pjnmopi  22783  sumdmdlem  23053  esumpcvgval  23644  soseq  24639  elfix  24828  ax5seglem5  24947  btwnconn1lem7  25102  ovoliunnfl  25315  ivthALT  25407  topfneec  25440  fdc  25604  ismtyres  25680  isdrngo3  25738  isnumbasgrplem3  26418  pm13.13b  26756  wlkdvspthlem  27503  a9e2ndeqALT  28219  bnj545  28438  bnj900  28472  bnj1498  28602  lshpset2N  29127  3dimlem1  29465  3dim3  29476  cdleme31fv2  30400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator