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  2041  barbari  2102  cesaro  2108  camestros  2109  calemos  2119  swopo  4236  elrnrexdm  5567  tfrcl  6269  ixpsnf1o  6638  fidcenumlemrk  6850  subhalfnqq  7246  enq0ref  7265  prarloc  7335  letrp1  8630  p1le  8631  peano2uz2  9182  uzind  9186  uzid  9364  qreccl  9461