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  3507  eusv2nf  5357  dfpo2  6298  trsuc  6451  fo00  6859  eqfnov2  7548  caovmo  7656  bropopvvv  8099  tz7.48lemOLD  8444  tz7.48-1  8446  oewordri  8594  epfrs  9725  ordpipq  11020  ltexprlem4  11117  xrinfmsslem  13431  hashfzp1  14569  dfgcd2  16712  catpropd  17876  idmgmhm  18883  symg2bas  19600  psgndiflemB  21899  pmatcollpw2lem  23088  icccvx  25264  uspgr1v1eop  29823  esumcst  34688  ddemeas  34862  bnj600  35542  bnj852  35544  satfvsucsuc  36109  satffunlem2lem2  36150  satffunlem2  36152  bj-csbsnlem  37795  bj-elid6  38071  aks6d1c6isolem3  43206  nzss  45286  iotasbc  45388  wallispilem3  47046  dfafv2  48171  nnsum3primes4  48855