Theorem ancli 321

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  pm4.45im  332  mo23  2055  barbari  2116  cesaro  2122  camestros  2123  calemos  2133  swopo  4284  elrnrexdm  5624  tfrcl  6332  ixpsnf1o  6702  fidcenumlemrk  6919  subhalfnqq  7355  enq0ref  7374  prarloc  7444  letrp1  8743  p1le  8744  peano2uz2  9298  uzind  9302  uzid  9480  qreccl  9580  fprodsplit1f  11575