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  3518  eusv2nf  5362  dfpo2  6282  trsuc  6437  fo00  6850  eqfnov2  7531  caovmo  7638  bropopvvv  8083  tz7.48lem  8449  tz7.48-1  8451  oewordri  8598  epfrs  9737  ordpipq  10948  ltexprlem4  11045  xrinfmsslem  13316  hashfzp1  14437  dfgcd2  16550  catpropd  17706  idmgmhm  18664  symg2bas  19359  psgndiflemB  21545  pmatcollpw2lem  22700  icccvx  24884  uspgr1v1eop  29160  esumcst  34002  ddemeas  34175  bnj600  34871  bnj852  34873  satfvsucsuc  35308  satffunlem2lem2  35349  satffunlem2  35351  bj-csbsnlem  36842  bj-elid6  37109  aks6d1c6isolem3  42111  nzss  44267  iotasbc  44369  wallispilem3  46026  dfafv2  47089  nnsum3primes4  47720