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 ) )

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  2122  barbari  2183  cesaro  2189  camestros  2190  calemos  2200  swopo  4427  elrnrexdm  5816  uchoice  6331  tfrcl  6595  ixpsnf1o  6971  fidcenumlemrk  7224  subhalfnqq  7729  enq0ref  7748  prarloc  7818  letrp1  9122  p1le  9123  peano2uz2  9685  uzind  9689  uzid  9868  qreccl  9974  fprodsplit1f  12320  lmodfopne  14474  wlkres  16374