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  3507  eusv2nf  5350  dfpo2  6269  trsuc  6421  fo00  6836  eqfnov2  7519  caovmo  7626  bropopvvv  8069  tz7.48lem  8409  tz7.48-1  8411  oewordri  8556  epfrs  9684  ordpipq  10895  ltexprlem4  10992  xrinfmsslem  13268  hashfzp1  14396  dfgcd2  16516  catpropd  17670  idmgmhm  18628  symg2bas  19323  psgndiflemB  21509  pmatcollpw2lem  22664  icccvx  24848  uspgr1v1eop  29176  esumcst  34053  ddemeas  34226  bnj600  34909  bnj852  34911  satfvsucsuc  35352  satffunlem2lem2  35393  satffunlem2  35395  bj-csbsnlem  36891  bj-elid6  37158  aks6d1c6isolem3  42164  nzss  44306  iotasbc  44408  wallispilem3  46065  dfafv2  47133  nnsum3primes4  47789