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  2086  barbari  2147  cesaro  2153  camestros  2154  calemos  2164  swopo  4342  elrnrexdm  5702  uchoice  6197  tfrcl  6424  ixpsnf1o  6797  fidcenumlemrk  7022  subhalfnqq  7484  enq0ref  7503  prarloc  7573  letrp1  8878  p1le  8879  peano2uz2  9436  uzind  9440  uzid  9618  qreccl  9719  fprodsplit1f  11802  lmodfopne  13908