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  3540  eusv2nf  5400  dfpo2  6317  trsuc  6472  fo00  6884  eqfnov2  7562  caovmo  7669  bropopvvv  8113  tz7.48lem  8479  tz7.48-1  8481  oewordri  8628  epfrs  9768  ordpipq  10979  ltexprlem4  11076  xrinfmsslem  13346  hashfzp1  14466  dfgcd2  16579  catpropd  17753  idmgmhm  18726  symg2bas  19424  psgndiflemB  21635  pmatcollpw2lem  22798  icccvx  24994  uspgr1v1eop  29280  esumcst  34043  ddemeas  34216  bnj600  34911  bnj852  34913  satfvsucsuc  35349  satffunlem2lem2  35390  satffunlem2  35392  bj-csbsnlem  36885  bj-elid6  37152  aks6d1c6isolem3  42157  nzss  44312  iotasbc  44414  wallispilem3  46022  dfafv2  47081  nnsum3primes4  47712