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

Theorem ancri 552
Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
ancri.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
ancri  |-  ( ph  ->  ( ps  /\  ph ) )

Proof of Theorem ancri
StepHypRef Expression
1 ancri.1 . 2  |-  ( ph  ->  ps )
2 id 22 . 2  |-  ( ph  ->  ph )
31, 2jca 532 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ 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:  truanOLD  1397  bamalip  2429  gencbvex  3157  eusv2nf  4645  trsuc  4962  issref  5380  fo00  5849  eqfnov2  6394  caovmo  6497  bropopvvv  6864  tz7.48lem  7107  tz7.48-1  7109  oewordri  7242  epfrs  8163  ordpipq  9321  ltexprlem4  9418  xrinfmsslem  11500  hash2prv  12492  swrdccat3a  12685  catpropd  14968  symg2bas  16237  psgndiflemB  18443  pmatcollpw2lem  19085  chpmat1dlem  19143  icccvx  21277  0wlkon  24322  2wlkonot3v  24648  2spthonot3v  24649  esumcst  27822  ddemeas  27959  dfpo2  29037  wl-sbal1  29866  nzss  31049  iotasbc  31131  wallispilem3  31594  bnj600  33273  bnj852  33275  bj-csbsnlem  33768
  Copyright terms: Public domain W3C validator