Theorem ancli 323

Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)

Hypothesis

Ref	Expression
ancli.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ancli	⊢ (𝜑 → (𝜑 ∧ 𝜓))

Proof of Theorem ancli

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜑 → 𝜑)
2		ancli.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	jca 306	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  pm4.45im  334  mo23  2097  barbari  2158  cesaro  2164  camestros  2165  calemos  2175  swopo  4371  elrnrexdm  5742  uchoice  6246  tfrcl  6473  ixpsnf1o  6846  fidcenumlemrk  7082  subhalfnqq  7562  enq0ref  7581  prarloc  7651  letrp1  8956  p1le  8957  peano2uz2  9515  uzind  9519  uzid  9697  qreccl  9798  fprodsplit1f  12060  lmodfopne  14203