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

Theorem ancri 552
Description: Deduction conjoining antecedent to right of consequent. (Contributed by NM, 15-Aug-1994.)
Hypothesis
Ref Expression
ancri.1
Assertion
Ref Expression
ancri

Proof of Theorem ancri
StepHypRef Expression
1 ancri.1 . 2
2 id 22 . 2
31, 2jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  truanOLD  1413  bamalip  2419  gencbvex  3153  eusv2nf  4650  trsuc  4967  issref  5385  fo00  5854  eqfnov2  6409  caovmo  6512  bropopvvv  6880  tz7.48lem  7125  tz7.48-1  7127  oewordri  7260  epfrs  8183  ordpipq  9341  ltexprlem4  9438  xrinfmsslem  11528  hash2prv  12525  swrdccat3a  12719  catpropd  15104  idmhm  15975  symg2bas  16423  psgndiflemB  18636  pmatcollpw2lem  19278  icccvx  21450  0wlkon  24549  2wlkonot3v  24875  2spthonot3v  24876  esumcst  28071  ddemeas  28208  dfpo2  29184  nzss  31222  iotasbc  31326  wallispilem3  31849  idmgmhm  32476  bnj600  33977  bnj852  33979  bj-csbsnlem  34470
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
  Copyright terms: Public domain W3C validator