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  3501  eusv2nf  5342  dfpo2  6262  trsuc  6414  fo00  6818  eqfnov2  7498  caovmo  7605  bropopvvv  8042  tz7.48lem  8382  tz7.48-1  8384  oewordri  8530  epfrs  9652  ordpipq  10865  ltexprlem4  10962  xrinfmsslem  13235  hashfzp1  14366  dfgcd2  16485  catpropd  17644  idmgmhm  18638  symg2bas  19334  psgndiflemB  21567  pmatcollpw2lem  22733  icccvx  24916  uspgr1v1eop  29334  esumcst  34241  ddemeas  34414  bnj600  35095  bnj852  35097  satfvsucsuc  35581  satffunlem2lem2  35622  satffunlem2  35624  bj-csbsnlem  37151  bj-elid6  37425  aks6d1c6isolem3  42546  nzss  44673  iotasbc  44775  wallispilem3  46425  dfafv2  47492  nnsum3primes4  48148