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 514	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  gencbvex  3541  eusv2nf  5282  trsuc  6261  fo00  6636  eqfnov2  7267  caovmo  7371  bropopvvv  7771  tz7.48lem  8063  tz7.48-1  8065  oewordri  8204  epfrs  9159  ordpipq  10350  ltexprlem4  10447  xrinfmsslem  12688  hashfzp1  13782  dfgcd2  15877  catpropd  16962  symg2bas  18504  psgndiflemB  20727  pmatcollpw2lem  21368  icccvx  23537  uspgr1v1eop  27017  esumcst  31329  ddemeas  31502  bnj600  32198  bnj852  32200  satfvsucsuc  32619  satffunlem2lem2  32660  satffunlem2  32662  dfpo2  32998  bj-csbsnlem  34236  bj-elid6  34478  nzss  40739  iotasbc  40841  wallispilem3  42442  dfafv2  43421  nnsum3primes4  44038  idmgmhm  44140