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  3541  eusv2nf  5395  dfpo2  6316  trsuc  6471  fo00  6884  eqfnov2  7563  caovmo  7670  bropopvvv  8115  tz7.48lem  8481  tz7.48-1  8483  oewordri  8630  epfrs  9771  ordpipq  10982  ltexprlem4  11079  xrinfmsslem  13350  hashfzp1  14470  dfgcd2  16583  catpropd  17752  idmgmhm  18714  symg2bas  19410  psgndiflemB  21618  pmatcollpw2lem  22783  icccvx  24981  uspgr1v1eop  29266  esumcst  34064  ddemeas  34237  bnj600  34933  bnj852  34935  satfvsucsuc  35370  satffunlem2lem2  35411  satffunlem2  35413  bj-csbsnlem  36904  bj-elid6  37171  aks6d1c6isolem3  42177  nzss  44336  iotasbc  44438  wallispilem3  46082  dfafv2  47144  nnsum3primes4  47775