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  2124  barbari  2185  cesaro  2191  camestros  2192  calemos  2202  swopo  4429  elrnrexdm  5818  uchoice  6333  tfrcl  6597  ixpsnf1o  6973  fidcenumlemrk  7226  subhalfnqq  7731  enq0ref  7750  prarloc  7820  letrp1  9124  p1le  9125  peano2uz2  9688  uzind  9692  uzid  9871  qreccl  9977  fprodsplit1f  12324  lmodfopne  14491  wlkres  16391