Theorem ancri 549

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  gencbvex  3478  eusv2nf  5313  dfpo2  6188  trsuc  6335  fo00  6735  eqfnov2  7382  caovmo  7487  bropopvvv  7901  tz7.48lem  8242  tz7.48-1  8244  oewordri  8385  epfrs  9420  ordpipq  10629  ltexprlem4  10726  xrinfmsslem  12971  hashfzp1  14074  dfgcd2  16182  catpropd  17335  symg2bas  18915  psgndiflemB  20717  pmatcollpw2lem  21834  icccvx  24019  uspgr1v1eop  27519  esumcst  31931  ddemeas  32104  bnj600  32799  bnj852  32801  satfvsucsuc  33227  satffunlem2lem2  33268  satffunlem2  33270  bj-csbsnlem  35015  bj-elid6  35268  nzss  41824  iotasbc  41926  wallispilem3  43498  dfafv2  44511  nnsum3primes4  45128  idmgmhm  45230