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  2047  barbari  2108  cesaro  2114  camestros  2115  calemos  2125  swopo  4266  elrnrexdm  5606  tfrcl  6311  ixpsnf1o  6681  fidcenumlemrk  6898  subhalfnqq  7334  enq0ref  7353  prarloc  7423  letrp1  8719  p1le  8720  peano2uz2  9271  uzind  9275  uzid  9453  qreccl  9551  fprodsplit1f  11531