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  2095  barbari  2156  cesaro  2162  camestros  2163  calemos  2173  swopo  4353  elrnrexdm  5719  uchoice  6223  tfrcl  6450  ixpsnf1o  6823  fidcenumlemrk  7056  subhalfnqq  7527  enq0ref  7546  prarloc  7616  letrp1  8921  p1le  8922  peano2uz2  9480  uzind  9484  uzid  9662  qreccl  9763  fprodsplit1f  11945  lmodfopne  14088