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  3487  eusv2nf  5337  dfpo2  6260  trsuc  6412  fo00  6816  eqfnov2  7497  caovmo  7604  bropopvvv  8040  tz7.48lem  8380  tz7.48-1  8382  oewordri  8528  epfrs  9652  ordpipq  10865  ltexprlem4  10962  xrinfmsslem  13260  hashfzp1  14393  dfgcd2  16515  catpropd  17675  idmgmhm  18669  symg2bas  19368  psgndiflemB  21580  pmatcollpw2lem  22742  icccvx  24917  uspgr1v1eop  29318  esumcst  34207  ddemeas  34380  bnj600  35061  bnj852  35063  satfvsucsuc  35547  satffunlem2lem2  35588  satffunlem2  35590  bj-csbsnlem  37210  bj-elid6  37484  aks6d1c6isolem3  42615  nzss  44744  iotasbc  44846  wallispilem3  46495  dfafv2  47580  nnsum3primes4  48264