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

Theorem biimparc 487
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 225 . 2  |-  ( ch 
->  ( ph  ->  ps ) )
32imp 429 1  |-  ( ( ch  /\  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  biantr  929  elrab3t  3260  difprsnss  4162  elpw2g  4610  elon2  4889  ideqg  5153  elrnmpt1s  5249  elrnmptg  5251  eqfnfv2  5975  fmpt  6041  elunirn  6150  fun11iun  6744  tposfo2  6978  tposf12  6980  dom2lem  7555  enfii  7737  ssnnfi  7739  ac6sfi  7763  unfilem1  7783  inf3lem2  8045  infdiffi  8073  dfac5lem5  8507  dfac2  8510  dfac12k  8526  cfslb2n  8647  enfin2i  8700  fin23lem19  8715  axdc2lem  8827  axdc3lem4  8832  winainflem  9070  gruiun  9176  indpi  9284  ltexnq  9352  ltbtwnnq  9355  ltexprlem6  9418  prlem936  9424  elreal2  9508  fimaxre3  10491  expnbnd  12262  repswswrd  12718  climcnds  13625  unbenlem  14284  acsfn  14913  lsmcv  17582  maducoeval2  18925  bastop2  19278  neipeltop  19412  rnelfmlem  20204  isfcls  20261  tgphaus  20366  mbfi1fseqlem4  21876  ulm2  22530  ax5seglem5  23928  wlkdvspthlem  24301  wlknwwlknsur  24404  spanunsni  26189  nonbooli  26261  nmopun  26625  lncnopbd  26648  pjnmopi  26759  sumdmdlem  27029  spc2ed  27064  rnmpt2ss  27203  esumpcvgval  27740  soseq  28927  btwnconn1lem7  29336  ovoliunnfl  29649  voliunnfl  29651  volsupnfl  29652  ivthALT  29746  topfneec  29779  fdc  29857  ismtyres  29923  isdrngo3  29981  isnumbasgrplem3  30674  pm13.13b  30909  ax6e2ndeqALT  32820  sineq0ALT  32826  bnj545  33041  bnj900  33075  bnj1498  33205  bj-snglss  33618  lshpset2N  33925  3dimlem1  34263  3dim3  34274  cdleme31fv2  35198
  Copyright terms: Public domain W3C validator