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  2077  barbari  2138  cesaro  2144  camestros  2145  calemos  2155  swopo  4318  elrnrexdm  5668  tfrcl  6378  ixpsnf1o  6749  fidcenumlemrk  6966  subhalfnqq  7426  enq0ref  7445  prarloc  7515  letrp1  8818  p1le  8819  peano2uz2  9373  uzind  9377  uzid  9555  qreccl  9655  fprodsplit1f  11655  lmodfopne  13510