Theorem ancri 550

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  gencbvex  3488  eusv2nf  5318  dfpo2  6199  trsuc  6350  fo00  6752  eqfnov2  7404  caovmo  7509  bropopvvv  7930  tz7.48lem  8272  tz7.48-1  8274  oewordri  8423  epfrs  9489  ordpipq  10698  ltexprlem4  10795  xrinfmsslem  13042  hashfzp1  14146  dfgcd2  16254  catpropd  17418  symg2bas  19000  psgndiflemB  20805  pmatcollpw2lem  21926  icccvx  24113  uspgr1v1eop  27616  esumcst  32031  ddemeas  32204  bnj600  32899  bnj852  32901  satfvsucsuc  33327  satffunlem2lem2  33368  satffunlem2  33370  bj-csbsnlem  35088  bj-elid6  35341  nzss  41935  iotasbc  42037  wallispilem3  43608  dfafv2  44624  nnsum3primes4  45240  idmgmhm  45342