Theorem ancri 552

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  gencbvex  3551  eusv2nf  5298  trsuc  6277  fo00  6652  eqfnov2  7283  caovmo  7387  bropopvvv  7787  tz7.48lem  8079  tz7.48-1  8081  oewordri  8220  epfrs  9175  ordpipq  10366  ltexprlem4  10463  xrinfmsslem  12704  hashfzp1  13795  dfgcd2  15896  catpropd  16981  symg2bas  18523  psgndiflemB  20746  pmatcollpw2lem  21387  icccvx  23556  uspgr1v1eop  27033  esumcst  31324  ddemeas  31497  bnj600  32193  bnj852  32195  satfvsucsuc  32614  satffunlem2lem2  32655  satffunlem2  32657  dfpo2  32993  bj-csbsnlem  34222  bj-elid6  34464  nzss  40656  iotasbc  40758  wallispilem3  42359  dfafv2  43338  nnsum3primes4  43960  idmgmhm  44062