Theorem ancri 558

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 23	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	jca 520	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  gencbvex  3519  eusv2nf  5367  dfpo2  6298  trsuc  6451  fo00  6858  eqfnov2  7541  caovmo  7648  bropopvvv  8084  tz7.48lem  8427  tz7.48-1  8429  oewordri  8577  epfrs  9699  ordpipq  10926  ltexprlem4  11023  xrinfmsslem  13333  hashfzp1  14467  dfgcd2  16603  catpropd  17764  idmgmhm  18758  symg2bas  19462  psgndiflemB  21718  pmatcollpw2lem  22902  icccvx  25077  uspgr1v1eop  29539  esumcst  34397  ddemeas  34570  bnj600  35251  bnj852  35253  satfvsucsuc  35755  satffunlem2lem2  35796  satffunlem2  35798  bj-csbsnlem  37426  bj-elid6  37701  aks6d1c6isolem3  42832  nzss  44918  iotasbc  45020  wallispilem3  46672  dfafv2  47757  nnsum3primes4  48441