Theorem ancli 323

Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)

Hypothesis

Ref	Expression
ancli.1	|- ( ph -> ps )

Assertion

Ref	Expression
ancli	|- ( ph -> ( ph /\ ps ) )

Proof of Theorem ancli

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2		ancli.1	. 2 |- ( ph -> ps )
3	1, 2	jca 306	1 |- ( ph -> ( ph /\ ps ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  pm4.45im  334  mo23  2128  barbari  2189  cesaro  2195  camestros  2196  calemos  2206  swopo  4451  elrnrexdm  5847  uchoice  6371  tfrcl  6635  ixpsnf1o  7018  fidcenumlemrk  7271  subhalfnqq  7781  enq0ref  7800  prarloc  7870  letrp1  9180  p1le  9181  peano2uz2  9757  uzind  9761  uzid  9945  qreccl  10051  fprodsplit1f  12417  lmodfopne  14712  wlkres  16718