Theorem ancri 550

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 512	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  gencbvex  3535  eusv2nf  5393  dfpo2  6295  trsuc  6451  fo00  6869  eqfnov2  7538  caovmo  7643  bropopvvv  8075  tz7.48lem  8440  tz7.48-1  8442  oewordri  8591  epfrs  9725  ordpipq  10936  ltexprlem4  11033  xrinfmsslem  13286  hashfzp1  14390  dfgcd2  16487  catpropd  17652  symg2bas  19259  psgndiflemB  21152  pmatcollpw2lem  22278  icccvx  24465  uspgr1v1eop  28503  esumcst  33056  ddemeas  33229  bnj600  33925  bnj852  33927  satfvsucsuc  34351  satffunlem2lem2  34392  satffunlem2  34394  bj-csbsnlem  35778  bj-elid6  36046  nzss  43066  iotasbc  43168  wallispilem3  44773  dfafv2  45830  nnsum3primes4  46446  idmgmhm  46548