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  5357  dfpo2  6302  trsuc  6455  fo00  6866  eqfnov2  7554  caovmo  7662  bropopvvv  8105  tz7.48lemOLD  8458  tz7.48-1  8460  oewordri  8608  epfrs  9739  ordpipq  11034  ltexprlem4  11131  xrinfmsslem  13445  hashfzp1  14583  dfgcd2  16728  catpropd  17892  idmgmhm  18899  symg2bas  19616  psgndiflemB  21915  pmatcollpw2lem  23104  icccvx  25280  uspgr1v1eop  29839  esumcst  34745  ddemeas  34919  bnj600  35599  bnj852  35601  satfvsucsuc  36220  satffunlem2lem2  36261  satffunlem2  36263  bj-csbsnlem  37911  bj-elid6  38200  aks6d1c6isolem3  43335  nzss  45410  iotasbc  45511  wallispilem3  47185  dfafv2  48310  nnsum3primes4  48994