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:  bamalip  2263  gencbvex  2830  trsuc  4476  eusv2nf  4532  issref  5056  fo00  5509  eqfnov2  5951  caovmo  6057  tz7.48lem  6453  tz7.48-1  6455  oewordri  6590  epfrs  7413  ordpipq  8566  ltexprlem4  8663  xrinfmsslem  10626  catpropd  13612  icccvx  18448  esumcst  23436  dfpo2  24112  trcrm  24951  iotasbc  27619  wallispilem3  27816  bnj600  28951  bnj852  28953
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