Theorem ancri 551

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  gencbvex  3536  eusv2nf  5394  dfpo2  6296  trsuc  6452  fo00  6870  eqfnov2  7539  caovmo  7644  bropopvvv  8076  tz7.48lem  8441  tz7.48-1  8443  oewordri  8592  epfrs  9726  ordpipq  10937  ltexprlem4  11034  xrinfmsslem  13287  hashfzp1  14391  dfgcd2  16488  catpropd  17653  symg2bas  19260  psgndiflemB  21153  pmatcollpw2lem  22279  icccvx  24466  uspgr1v1eop  28506  esumcst  33061  ddemeas  33234  bnj600  33930  bnj852  33932  satfvsucsuc  34356  satffunlem2lem2  34397  satffunlem2  34399  bj-csbsnlem  35783  bj-elid6  36051  nzss  43076  iotasbc  43178  wallispilem3  44783  dfafv2  45840  nnsum3primes4  46456  idmgmhm  46558