Theorem ancri 559

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  gencbvex  3513  eusv2nf  5368  dfpo2  6301  trsuc  6454  fo00  6861  eqfnov2  7549  caovmo  7657  bropopvvv  8091  tz7.48lem  8434  tz7.48-1  8436  oewordri  8584  epfrs  9707  ordpipq  10942  ltexprlem4  11039  xrinfmsslem  13350  hashfzp1  14486  dfgcd2  16626  catpropd  17787  idmgmhm  18791  symg2bas  19507  psgndiflemB  21800  pmatcollpw2lem  22984  icccvx  25160  uspgr1v1eop  29657  esumcst  34517  ddemeas  34691  bnj600  35372  bnj852  35374  satfvsucsuc  35894  satffunlem2lem2  35935  satffunlem2  35937  bj-csbsnlem  37595  bj-elid6  37871  aks6d1c6isolem3  43001  nzss  45085  iotasbc  45187  wallispilem3  46839  dfafv2  47927  nnsum3primes4  48611