Theorem ancri 558

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  gencbvex  3511  eusv2nf  5366  dfpo2  6297  trsuc  6450  fo00  6857  eqfnov2  7540  caovmo  7647  bropopvvv  8081  tz7.48lem  8424  tz7.48-1  8426  oewordri  8574  epfrs  9696  ordpipq  10922  ltexprlem4  11019  xrinfmsslem  13329  hashfzp1  14464  dfgcd2  16599  catpropd  17760  idmgmhm  18754  symg2bas  19458  psgndiflemB  21750  pmatcollpw2lem  22934  icccvx  25109  uspgr1v1eop  29599  esumcst  34453  ddemeas  34626  bnj600  35307  bnj852  35309  satfvsucsuc  35857  satffunlem2lem2  35898  satffunlem2  35900  bj-csbsnlem  37538  bj-elid6  37814  aks6d1c6isolem3  42943  nzss  45027  iotasbc  45129  wallispilem3  46781  dfafv2  47869  nnsum3primes4  48553