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

Theorem ancri 555
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 535 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  bamalip  2414  gencbvex  3091  eusv2nf  4600  issref  5212  trsuc  5506  fo00  5846  eqfnov2  6400  caovmo  6503  bropopvvv  6871  tz7.48lem  7155  tz7.48-1  7157  oewordri  7290  epfrs  8212  ordpipq  9364  ltexprlem4  9461  xrinfmsslem  11590  swrdccat3a  12845  catpropd  15607  idmhm  16584  symg2bas  17032  psgndiflemB  19161  pmatcollpw2lem  19794  icccvx  21971  0wlkon  25270  2wlkonot3v  25596  2spthonot3v  25597  esumcst  28877  ddemeas  29052  bnj600  29723  bnj852  29725  dfpo2  30388  bj-csbsnlem  31498  nzss  36660  iotasbc  36764  wallispilem3  37923  nnsum3primes4  38877  uspgr1v1eop  39309  idmgmhm  39775
  Copyright terms: Public domain W3C validator