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  2067  barbari  2128  cesaro  2134  camestros  2135  calemos  2145  swopo  4307  elrnrexdm  5656  tfrcl  6365  ixpsnf1o  6736  fidcenumlemrk  6953  subhalfnqq  7413  enq0ref  7432  prarloc  7502  letrp1  8805  p1le  8806  peano2uz2  9360  uzind  9364  uzid  9542  qreccl  9642  fprodsplit1f  11642  lmodfopne  13416