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  difprsn  3756  elpw2g  4174  elon2  4403  ideqg  4835  elrnmpt1s  4927  elrnmptg  4929  fun11iun  5493  eqfnfv2  5623  fmpt  5681  elunirnALT  5779  tposfo2  6257  tposf12  6259  dom2lem  6901  enfii  7080  ssnnfi  7082  ac6sfi  7101  unfilem1  7121  inf3lem2  7330  infdiffi  7358  dfac5lem5  7754  dfac2  7757  dfac12k  7773  cfslb2n  7894  enfin2i  7947  fin23lem19  7962  axdc2lem  8074  axdc3lem4  8079  winainflem  8315  gruiun  8421  indpi  8531  ltexnq  8599  ltbtwnnq  8602  ltexprlem6  8665  prlem936  8671  elreal2  8754  fimaxre3  9703  expnbnd  11230  climcnds  12310  unbenlem  12955  acsfn  13561  lsmcv  15894  bastop2  16732  rnelfmlem  17647  isfcls  17704  tgphaus  17799  mbfi1fseqlem4  19073  ulm2  19764  spanunsni  22158  nonbooli  22230  nmopun  22594  lncnopbd  22617  pjnmopi  22728  sumdmdlem  22998  esumpcvgval  23446  soseq  24254  elfix  24443  ax5seglem5  24561  btwnconn1lem7  24716  ivthALT  26258  topfneec  26291  fdc  26455  ismtyres  26532  isdrngo3  26590  isnumbasgrplem3  27270  pm13.13b  27608  a9e2ndeqALT  28708  bnj545  28927  bnj900  28961  bnj1498  29091  lshpset2N  29309  3dimlem1  29647  3dim3  29658  cdleme31fv2  30582
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