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  3495  eusv2nf  5328  dfpo2  6238  trsuc  6390  fo00  6794  eqfnov2  7471  caovmo  7578  bropopvvv  8015  tz7.48lem  8355  tz7.48-1  8357  oewordri  8502  epfrs  9616  ordpipq  10828  ltexprlem4  10925  xrinfmsslem  13202  hashfzp1  14333  dfgcd2  16452  catpropd  17610  idmgmhm  18604  symg2bas  19300  psgndiflemB  21532  pmatcollpw2lem  22687  icccvx  24870  uspgr1v1eop  29222  esumcst  34068  ddemeas  34241  bnj600  34923  bnj852  34925  satfvsucsuc  35401  satffunlem2lem2  35442  satffunlem2  35444  bj-csbsnlem  36937  bj-elid6  37204  aks6d1c6isolem3  42209  nzss  44350  iotasbc  44452  wallispilem3  46105  dfafv2  47163  nnsum3primes4  47819