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

Theorem ancri 535
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 19 . 2  |-  ( ph  ->  ph )
31, 2jca 518 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  truan  1331  bamalip  2329  gencbvex  2906  trsuc  4558  eusv2nf  4614  issref  5138  fo00  5592  eqfnov2  6038  caovmo  6144  tz7.48lem  6540  tz7.48-1  6542  oewordri  6677  epfrs  7503  ordpipq  8656  ltexprlem4  8753  xrinfmsslem  10718  catpropd  13711  icccvx  18552  esumcst  23721  dfpo2  24670  iotasbc  26942  wallispilem3  27139  bropopvvv  27435  0wlkon  27699  bnj600  28713  bnj852  28715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator