Theorem ancri 576

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 555	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  bamalip  2724  gencbvex  3390  eusv2nf  5013  issref  5667  trsuc  5971  fo00  6334  eqfnov2  6933  caovmo  7037  bropopvvv  7424  tz7.48lem  7706  tz7.48-1  7708  oewordri  7843  epfrs  8782  ordpipq  9976  ltexprlem4  10073  xrinfmsslem  12351  hashfzp1  13430  swrdccat3a  13714  dfgcd2  15485  catpropd  16590  idmhm  17565  symg2bas  18038  psgndiflemB  20168  pmatcollpw2lem  20804  icccvx  22970  uspgr1v1eop  26361  esumcst  30455  ddemeas  30629  bnj600  31317  bnj852  31319  dfpo2  31973  bj-csbsnlem  33220  bj-ismooredr2  33389  nzss  39036  iotasbc  39140  wallispilem3  40805  nnsum3primes4  42204  idmgmhm  42316