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  2079  barbari  2140  cesaro  2146  camestros  2147  calemos  2157  swopo  4321  elrnrexdm  5672  tfrcl  6384  ixpsnf1o  6755  fidcenumlemrk  6973  subhalfnqq  7433  enq0ref  7452  prarloc  7522  letrp1  8825  p1le  8826  peano2uz2  9380  uzind  9384  uzid  9562  qreccl  9662  fprodsplit1f  11662  lmodfopne  13610