Theorem ancri 554

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 516	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 208  df-an 397

This theorem is referenced by:  gencbvex  3488  eusv2nf  5324  dfpo2  6247  trsuc  6399  fo00  6803  eqfnov2  7486  caovmo  7593  bropopvvv  8029  tz7.48lem  8370  tz7.48-1  8372  oewordri  8518  epfrs  9643  ordpipq  10856  ltexprlem4  10953  xrinfmsslem  13251  hashfzp1  14384  dfgcd2  16506  catpropd  17666  idmgmhm  18660  symg2bas  19359  psgndiflemB  21575  pmatcollpw2lem  22760  icccvx  24935  uspgr1v1eop  29336  esumcst  34247  ddemeas  34420  bnj600  35101  bnj852  35103  satfvsucsuc  35593  satffunlem2lem2  35634  satffunlem2  35636  bj-csbsnlem  37256  bj-elid6  37530  aks6d1c6isolem3  42661  nzss  44761  iotasbc  44863  wallispilem3  46510  dfafv2  47595  nnsum3primes4  48279