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

Theorem ancri 554
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 23 . 2  |-  ( ph  ->  ph )
31, 2jca 534 1  |-  ( ph  ->  ( ps  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  truanOLD  1455  bamalip  2382  gencbvex  3122  eusv2nf  4614  issref  5224  trsuc  5517  fo00  5855  eqfnov2  6408  caovmo  6511  bropopvvv  6878  tz7.48lem  7157  tz7.48-1  7159  oewordri  7292  epfrs  8205  ordpipq  9356  ltexprlem4  9453  xrinfmsslem  11582  hash2prv  12623  swrdccat3a  12824  catpropd  15566  idmhm  16543  symg2bas  16991  psgndiflemB  19105  pmatcollpw2lem  19738  icccvx  21900  0wlkon  25163  2wlkonot3v  25489  2spthonot3v  25490  esumcst  28764  ddemeas  28939  bnj600  29559  bnj852  29561  dfpo2  30223  bj-csbsnlem  31296  nzss  36351  iotasbc  36455  wallispilem3  37546  nnsum3primes4  38330  idmgmhm  38603
  Copyright terms: Public domain W3C validator