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

This theorem is referenced by:  gencbvex  3510  eusv2nf  5353  dfpo2  6272  trsuc  6424  fo00  6839  eqfnov2  7522  caovmo  7629  bropopvvv  8072  tz7.48lem  8412  tz7.48-1  8414  oewordri  8559  epfrs  9691  ordpipq  10902  ltexprlem4  10999  xrinfmsslem  13275  hashfzp1  14403  dfgcd2  16523  catpropd  17677  idmgmhm  18635  symg2bas  19330  psgndiflemB  21516  pmatcollpw2lem  22671  icccvx  24855  uspgr1v1eop  29183  esumcst  34060  ddemeas  34233  bnj600  34916  bnj852  34918  satfvsucsuc  35359  satffunlem2lem2  35400  satffunlem2  35402  bj-csbsnlem  36898  bj-elid6  37165  aks6d1c6isolem3  42171  nzss  44313  iotasbc  44415  wallispilem3  46072  dfafv2  47137  nnsum3primes4  47793