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  3504  eusv2nf  5345  dfpo2  6257  trsuc  6409  fo00  6818  eqfnov2  7499  caovmo  7606  bropopvvv  8046  tz7.48lem  8386  tz7.48-1  8388  oewordri  8533  epfrs  9660  ordpipq  10871  ltexprlem4  10968  xrinfmsslem  13244  hashfzp1  14372  dfgcd2  16492  catpropd  17646  idmgmhm  18604  symg2bas  19299  psgndiflemB  21485  pmatcollpw2lem  22640  icccvx  24824  uspgr1v1eop  29152  esumcst  34026  ddemeas  34199  bnj600  34882  bnj852  34884  satfvsucsuc  35325  satffunlem2lem2  35366  satffunlem2  35368  bj-csbsnlem  36864  bj-elid6  37131  aks6d1c6isolem3  42137  nzss  44279  iotasbc  44381  wallispilem3  46038  dfafv2  47106  nnsum3primes4  47762