Theorem ancri 546

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  bamalipOLD  2761  gencbvex  3438  eusv2nf  5065  idrefOLD  5727  trsuc  6025  fo00  6391  eqfnov2  7001  caovmo  7105  bropopvvv  7492  tz7.48lem  7775  tz7.48-1  7777  oewordri  7912  epfrs  8857  ordpipq  10052  ltexprlem4  10149  xrinfmsslem  12387  hashfzp1  13467  swrdccat3aOLD  13804  dfgcd2  15598  catpropd  16683  idmhm  17659  symg2bas  18130  psgndiflemB  20268  pmatcollpw2lem  20910  icccvx  23077  uspgr1v1eop  26483  esumcst  30641  ddemeas  30815  bnj600  31506  bnj852  31508  dfpo2  32159  bj-csbsnlem  33389  bj-ismooredr2  33558  nzss  39298  iotasbc  39401  wallispilem3  41027  dfafv2  41986  nnsum3primes4  42458  idmgmhm  42587