Theorem ancri 557

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  gencbvex  3509  eusv2nf  5349  dfpo2  6278  trsuc  6430  fo00  6838  eqfnov2  7521  caovmo  7628  bropopvvv  8063  tz7.48lem  8406  tz7.48-1  8408  oewordri  8556  epfrs  9680  ordpipq  10894  ltexprlem4  10991  xrinfmsslem  13305  hashfzp1  14438  dfgcd2  16571  catpropd  17732  idmgmhm  18726  symg2bas  19424  psgndiflemB  21640  pmatcollpw2lem  22825  icccvx  25000  uspgr1v1eop  29407  esumcst  34321  ddemeas  34494  bnj600  35175  bnj852  35177  satfvsucsuc  35676  satffunlem2lem2  35717  satffunlem2  35719  bj-csbsnlem  37349  bj-elid6  37623  aks6d1c6isolem3  42754  nzss  44854  iotasbc  44956  wallispilem3  46602  dfafv2  47687  nnsum3primes4  48371