Theorem ancri 573

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  bamalip  2574  gencbvex  3223  eusv2nf  4790  issref  5428  trsuc  5727  fo00  6084  eqfnov2  6665  caovmo  6769  bropopvvv  7142  tz7.48lem  7423  tz7.48-1  7425  oewordri  7559  epfrs  8490  ordpipq  9643  ltexprlem4  9740  xrinfmsslem  12010  hashfzp1  13078  swrdccat3a  13345  dfgcd2  15101  catpropd  16192  idmhm  17167  symg2bas  17641  psgndiflemB  19765  pmatcollpw2lem  20401  icccvx  22557  0wlkon  26077  2wlkonot3v  26402  2spthonot3v  26403  esumcst  29452  ddemeas  29626  bnj600  30243  bnj852  30245  dfpo2  30898  bj-csbsnlem  32090  nzss  37538  iotasbc  37642  wallispilem3  38960  nnsum3primes4  40204  uspgr1v1eop  40475  idmgmhm  41578