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  4397  elrnrexdm  5776  uchoice  6289  tfrcl  6516  ixpsnf1o  6891  fidcenumlemrk  7132  subhalfnqq  7612  enq0ref  7631  prarloc  7701  letrp1  9006  p1le  9007  peano2uz2  9565  uzind  9569  uzid  9748  qreccl  9849  fprodsplit1f  12161  lmodfopne  14306  wlkres  16123