Theorem ancri 559

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 23	. 2 ⊢ (𝜑 → 𝜑)
3	1, 2	jca 521	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  gencbvex  3506  eusv2nf  5360  dfpo2  6294  trsuc  6447  fo00  6854  eqfnov2  7543  caovmo  7651  bropopvvv  8087  tz7.48lem  8430  tz7.48-1  8432  oewordri  8580  epfrs  9710  ordpipq  10951  ltexprlem4  11048  xrinfmsslem  13360  hashfzp1  14496  dfgcd2  16636  catpropd  17797  idmgmhm  18803  symg2bas  19520  psgndiflemB  21813  pmatcollpw2lem  23002  icccvx  25178  uspgr1v1eop  29709  esumcst  34573  ddemeas  34747  bnj600  35428  bnj852  35430  satfvsucsuc  35944  satffunlem2lem2  35985  satffunlem2  35987  bj-csbsnlem  37646  bj-elid6  37922  aks6d1c6isolem3  43042  nzss  45141  iotasbc  45243  wallispilem3  46895  dfafv2  48020  nnsum3primes4  48704