Theorem ancri 574

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 553	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  2615  gencbvex  3281  eusv2nf  4894  issref  5544  trsuc  5848  fo00  6210  eqfnov2  6809  caovmo  6913  bropopvvv  7300  tz7.48lem  7581  tz7.48-1  7583  oewordri  7717  epfrs  8645  ordpipq  9802  ltexprlem4  9899  xrinfmsslem  12176  hashfzp1  13256  swrdccat3a  13540  dfgcd2  15310  catpropd  16416  idmhm  17391  symg2bas  17864  psgndiflemB  19994  pmatcollpw2lem  20630  icccvx  22796  uspgr1v1eop  26186  esumcst  30253  ddemeas  30427  bnj600  31115  bnj852  31117  dfpo2  31771  bj-csbsnlem  33023  bj-ismooredr2  33190  nzss  38833  iotasbc  38937  wallispilem3  40602  nnsum3primes4  42001  idmgmhm  42113