Theorem ancri 556

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 518	1 ⊢ (𝜑 → (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  gencbvex  3504  eusv2nf  5346  dfpo2  6272  trsuc  6424  fo00  6832  eqfnov2  7515  caovmo  7622  bropopvvv  8057  tz7.48lem  8400  tz7.48-1  8402  oewordri  8550  epfrs  9676  ordpipq  10890  ltexprlem4  10987  xrinfmsslem  13301  hashfzp1  14434  dfgcd2  16556  catpropd  17717  idmgmhm  18711  symg2bas  19409  psgndiflemB  21625  pmatcollpw2lem  22810  icccvx  24985  uspgr1v1eop  29389  esumcst  34314  ddemeas  34487  bnj600  35171  bnj852  35173  satfvsucsuc  35663  satffunlem2lem2  35704  satffunlem2  35706  bj-csbsnlem  37336  bj-elid6  37610  aks6d1c6isolem3  42741  nzss  44841  iotasbc  44943  wallispilem3  46589  dfafv2  47674  nnsum3primes4  48358