Theorem ancri 553

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  gencbvex  3497  eusv2nf  5261  trsuc  6243  fo00  6625  eqfnov2  7260  caovmo  7365  bropopvvv  7768  tz7.48lem  8060  tz7.48-1  8062  oewordri  8201  epfrs  9157  ordpipq  10353  ltexprlem4  10450  xrinfmsslem  12689  hashfzp1  13788  dfgcd2  15884  catpropd  16971  symg2bas  18513  psgndiflemB  20289  pmatcollpw2lem  21382  icccvx  23555  uspgr1v1eop  27039  esumcst  31432  ddemeas  31605  bnj600  32301  bnj852  32303  satfvsucsuc  32725  satffunlem2lem2  32766  satffunlem2  32768  dfpo2  33104  bj-csbsnlem  34344  bj-elid6  34585  nzss  41021  iotasbc  41123  wallispilem3  42709  dfafv2  43688  nnsum3primes4  44306  idmgmhm  44408