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  3510  eusv2nf  5364  dfpo2  6325  trsuc  6478  fo00  6892  eqfnov2  7581  caovmo  7690  bropopvvv  8136  tz7.48lemOLD  8489  tz7.48-1  8491  oewordri  8639  epfrs  9769  ordpipq  11066  ltexprlem4  11163  xrinfmsslem  13478  hashfzp1  14617  dfgcd2  16763  catpropd  17933  idmgmhm  18940  symg2bas  19658  psgndiflemB  21961  pmatcollpw2lem  23150  icccvx  25326  uspgr1v1eop  29887  esumcst  34806  ddemeas  34980  bnj600  35660  bnj852  35662  satfvsucsuc  36338  satffunlem2lem2  36379  satffunlem2  36381  bj-csbsnlem  38030  bj-elid6  38359  aks6d1c6isolem3  43492  nzss  45562  iotasbc  45663  wallispilem3  47350  dfafv2  48475  nnsum3primes4  49159