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  1387  bamalip  2407  gencbvex  3037  eusv2nf  4511  trsuc  4824  issref  5232  fo00  5695  eqfnov2  6218  caovmo  6321  bropopvvv  6674  tz7.48lem  6917  tz7.48-1  6919  oewordri  7052  epfrs  7972  ordpipq  9132  ltexprlem4  9229  xrinfmsslem  11291  swrdccat3a  12406  catpropd  14669  symg2bas  15924  psgndiflemB  18052  icccvx  20544  0wlkon  23468  esumcst  26536  ddemeas  26674  dfpo2  27587  wl-sbal1  28415  iotasbc  29699  wallispilem3  29888  hash2prv  30252  2wlkonot3v  30420  2spthonot3v  30421  pmatcollpw2lem  31120  bnj600  32008  bnj852  32010  bj-csbsnlem  32501
  Copyright terms: Public domain W3C validator