Theorem ancri 575

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

Step	Hyp	Ref	Expression
1		ancri.1	. 2 |- ( ph -> ps )
2		id 22	. 2 |- ( ph -> ph )
3	1, 2	jca 554	1 |- ( ph -> ( ps /\ ph ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  bamalip  2586  gencbvex  3250  eusv2nf  4864  issref  5509  trsuc  5810  fo00  6172  eqfnov2  6767  caovmo  6871  bropopvvv  7255  tz7.48lem  7536  tz7.48-1  7538  oewordri  7672  epfrs  8607  ordpipq  9764  ltexprlem4  9861  xrinfmsslem  12138  hashfzp1  13218  swrdccat3a  13494  dfgcd2  15263  catpropd  16369  idmhm  17344  symg2bas  17818  psgndiflemB  19946  pmatcollpw2lem  20582  icccvx  22749  uspgr1v1eop  26141  esumcst  30125  ddemeas  30299  bnj600  30989  bnj852  30991  dfpo2  31645  bj-csbsnlem  32898  bj-ismooredr2  33065  nzss  38516  iotasbc  38620  wallispilem3  40284  nnsum3primes4  41676  idmgmhm  41788