Theorem ancli 321

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 304	1 ⊢ (𝜑 → (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  pm4.45im  332  mo23  2038  barbari  2099  cesaro  2105  camestros  2106  calemos  2116  swopo  4223  elrnrexdm  5552  tfrcl  6254  ixpsnf1o  6623  fidcenumlemrk  6835  subhalfnqq  7215  enq0ref  7234  prarloc  7304  letrp1  8599  p1le  8600  peano2uz2  9151  uzind  9155  uzid  9333  qreccl  9427