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

This theorem is referenced by:  gencbvex  3532  eusv2nf  5389  dfpo2  6294  trsuc  6450  fo00  6869  eqfnov2  7545  caovmo  7652  bropopvvv  8089  tz7.48lem  8455  tz7.48-1  8457  oewordri  8606  epfrs  9748  ordpipq  10959  ltexprlem4  11056  xrinfmsslem  13313  hashfzp1  14416  dfgcd2  16515  catpropd  17682  idmgmhm  18654  symg2bas  19340  psgndiflemB  21525  pmatcollpw2lem  22672  icccvx  24868  uspgr1v1eop  29055  esumcst  33676  ddemeas  33849  bnj600  34544  bnj852  34546  satfvsucsuc  34969  satffunlem2lem2  35010  satffunlem2  35012  bj-csbsnlem  36375  bj-elid6  36643  aks6d1c6isolem3  41642  nzss  43748  iotasbc  43850  wallispilem3  45449  dfafv2  46506  nnsum3primes4  47122