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  2119  barbari  2180  cesaro  2186  camestros  2187  calemos  2197  swopo  4401  elrnrexdm  5782  uchoice  6295  tfrcl  6525  ixpsnf1o  6900  fidcenumlemrk  7144  subhalfnqq  7624  enq0ref  7643  prarloc  7713  letrp1  9018  p1le  9019  peano2uz2  9577  uzind  9581  uzid  9760  qreccl  9866  fprodsplit1f  12185  lmodfopne  14330  wlkres  16174