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  3496  eusv2nf  5337  dfpo2  6251  trsuc  6403  fo00  6807  eqfnov2  7485  caovmo  7592  bropopvvv  8029  tz7.48lem  8369  tz7.48-1  8371  oewordri  8516  epfrs  9632  ordpipq  10844  ltexprlem4  10941  xrinfmsslem  13214  hashfzp1  14345  dfgcd2  16464  catpropd  17623  idmgmhm  18617  symg2bas  19313  psgndiflemB  21546  pmatcollpw2lem  22712  icccvx  24895  uspgr1v1eop  29248  esumcst  34148  ddemeas  34321  bnj600  35003  bnj852  35005  satfvsucsuc  35481  satffunlem2lem2  35522  satffunlem2  35524  bj-csbsnlem  37020  bj-elid6  37287  aks6d1c6isolem3  42342  nzss  44474  iotasbc  44576  wallispilem3  46227  dfafv2  47294  nnsum3primes4  47950