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  2121  barbari  2182  cesaro  2188  camestros  2189  calemos  2199  swopo  4409  elrnrexdm  5794  uchoice  6309  tfrcl  6573  ixpsnf1o  6948  fidcenumlemrk  7196  subhalfnqq  7694  enq0ref  7713  prarloc  7783  letrp1  9087  p1le  9088  peano2uz2  9648  uzind  9652  uzid  9831  qreccl  9937  fprodsplit1f  12275  lmodfopne  14422  wlkres  16320