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  3498  eusv2nf  5337  dfpo2  6248  trsuc  6400  fo00  6804  eqfnov2  7483  caovmo  7590  bropopvvv  8030  tz7.48lem  8370  tz7.48-1  8372  oewordri  8517  epfrs  9646  ordpipq  10855  ltexprlem4  10952  xrinfmsslem  13229  hashfzp1  14357  dfgcd2  16476  catpropd  17634  idmgmhm  18594  symg2bas  19291  psgndiflemB  21526  pmatcollpw2lem  22681  icccvx  24865  uspgr1v1eop  29213  esumcst  34049  ddemeas  34222  bnj600  34905  bnj852  34907  satfvsucsuc  35357  satffunlem2lem2  35398  satffunlem2  35400  bj-csbsnlem  36896  bj-elid6  37163  aks6d1c6isolem3  42169  nzss  44310  iotasbc  44412  wallispilem3  46068  dfafv2  47136  nnsum3primes4  47792