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

Step	Hyp	Ref	Expression
1		ancri.1	. 2
2		id 22	. 2
3	1, 2	jca 532	1

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