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  3499  eusv2nf  5340  dfpo2  6254  trsuc  6406  fo00  6810  eqfnov2  7488  caovmo  7595  bropopvvv  8032  tz7.48lem  8372  tz7.48-1  8374  oewordri  8520  epfrs  9640  ordpipq  10853  ltexprlem4  10950  xrinfmsslem  13223  hashfzp1  14354  dfgcd2  16473  catpropd  17632  idmgmhm  18626  symg2bas  19322  psgndiflemB  21555  pmatcollpw2lem  22721  icccvx  24904  uspgr1v1eop  29322  esumcst  34220  ddemeas  34393  bnj600  35075  bnj852  35077  satfvsucsuc  35559  satffunlem2lem2  35600  satffunlem2  35602  bj-csbsnlem  37104  bj-elid6  37375  aks6d1c6isolem3  42430  nzss  44558  iotasbc  44660  wallispilem3  46311  dfafv2  47378  nnsum3primes4  48034