Theorem ancri 549

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  gencbvex  3520  eusv2nf  5365  dfpo2  6285  trsuc  6440  fo00  6853  eqfnov2  7535  caovmo  7642  bropopvvv  8087  tz7.48lem  8453  tz7.48-1  8455  oewordri  8602  epfrs  9743  ordpipq  10954  ltexprlem4  11051  xrinfmsslem  13322  hashfzp1  14447  dfgcd2  16563  catpropd  17719  idmgmhm  18677  symg2bas  19372  psgndiflemB  21558  pmatcollpw2lem  22713  icccvx  24897  uspgr1v1eop  29174  esumcst  34040  ddemeas  34213  bnj600  34896  bnj852  34898  satfvsucsuc  35333  satffunlem2lem2  35374  satffunlem2  35376  bj-csbsnlem  36867  bj-elid6  37134  aks6d1c6isolem3  42135  nzss  44289  iotasbc  44391  wallispilem3  46044  dfafv2  47109  nnsum3primes4  47750