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  931  elrab3t  3242  difprsnss  4150  elpw2g  4600  elon2  4879  ideqg  5144  elrnmpt1s  5240  elrnmptg  5242  eqfnfv2  5967  fmpt  6037  elunirn  6148  fun11iun  6745  tposfo2  6980  tposf12  6982  dom2lem  7557  enfii  7739  ssnnfi  7741  ac6sfi  7766  unfilem1  7786  inf3lem2  8049  infdiffi  8077  dfac5lem5  8511  dfac2  8514  dfac12k  8530  cfslb2n  8651  enfin2i  8704  fin23lem19  8719  axdc2lem  8831  axdc3lem4  8836  winainflem  9074  indpi  9288  ltexnq  9356  ltbtwnnq  9359  ltexprlem6  9422  prlem936  9428  elreal2  9512  fimaxre3  10499  expnbnd  12277  repswswrd  12738  climcnds  13645  fprod2dlem  13766  unbenlem  14408  acsfn  15038  lsmcv  17766  maducoeval2  19120  bastop2  19474  neipeltop  19608  rnelfmlem  20431  isfcls  20488  tgphaus  20593  mbfi1fseqlem4  22103  ulm2  22758  ax5seglem5  24214  wlkdvspthlem  24587  wlknwwlknsur  24690  spanunsni  26475  nonbooli  26547  nmopun  26911  lncnopbd  26934  pjnmopi  27045  sumdmdlem  27315  spc2ed  27350  rnmpt2ss  27493  esumpcvgval  28062  soseq  29310  btwnconn1lem7  29719  ovoliunnfl  30032  voliunnfl  30034  volsupnfl  30035  ivthALT  30129  topfneec  30149  fdc  30214  ismtyres  30280  isdrngo3  30338  isnumbasgrplem3  31030  pm13.13b  31269  fprodle  31558  ax6e2ndeqALT  33599  sineq0ALT  33605  bnj545  33821  bnj900  33855  bnj1498  33985  bj-snglss  34411  lshpset2N  34719  3dimlem1  35057  3dim3  35068  cdleme31fv2  35994
  Copyright terms: Public domain W3C validator