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  2402  gencbvex  3009  eusv2nf  4483  trsuc  4795  issref  5204  fo00  5667  eqfnov2  6192  caovmo  6295  bropopvvv  6648  tz7.48lem  6888  tz7.48-1  6890  oewordri  7023  epfrs  7943  ordpipq  9103  ltexprlem4  9200  xrinfmsslem  11262  swrdccat3a  12377  catpropd  14640  symg2bas  15892  psgndiflemB  17999  icccvx  20491  0wlkon  23391  esumcst  26462  ddemeas  26600  dfpo2  27512  wl-sbal1  28336  iotasbc  29616  wallispilem3  29805  hash2prv  30169  2wlkonot3v  30337  2spthonot3v  30338  bnj600  31769  bnj852  31771  bj-csbsnlem  32172
  Copyright terms: Public domain W3C validator