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  3488  eusv2nf  5332  dfpo2  6254  trsuc  6406  fo00  6810  eqfnov2  7490  caovmo  7597  bropopvvv  8033  tz7.48lem  8373  tz7.48-1  8375  oewordri  8521  epfrs  9643  ordpipq  10856  ltexprlem4  10953  xrinfmsslem  13251  hashfzp1  14384  dfgcd2  16506  catpropd  17666  idmgmhm  18660  symg2bas  19359  psgndiflemB  21590  pmatcollpw2lem  22752  icccvx  24927  uspgr1v1eop  29332  esumcst  34223  ddemeas  34396  bnj600  35077  bnj852  35079  satfvsucsuc  35563  satffunlem2lem2  35604  satffunlem2  35606  bj-csbsnlem  37226  bj-elid6  37500  aks6d1c6isolem3  42629  nzss  44762  iotasbc  44864  wallispilem3  46513  dfafv2  47592  nnsum3primes4  48276