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

Theorem ancri 536
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 20 . 2  |-  ( ph  ->  ph )
31, 2jca 519 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  truan  1337  bamalip  2382  gencbvex  2966  trsuc  4633  eusv2nf  4688  issref  5214  fo00  5678  eqfnov2  6144  caovmo  6251  bropopvvv  6393  tz7.48lem  6665  tz7.48-1  6667  oewordri  6802  epfrs  7631  ordpipq  8783  ltexprlem4  8880  xrinfmsslem  10850  catpropd  13898  icccvx  18936  0wlkon  21508  esumcst  24416  dfpo2  25334  iotasbc  27495  wallispilem3  27691  swrdccat3a  28038  2wlkonot3v  28080  2spthonot3v  28081  bnj600  29008  bnj852  29010
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 178  df-an 361
  Copyright terms: Public domain W3C validator