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  4453  elrnrexdm  5850  uchoice  6375  tfrcl  6639  ixpsnf1o  7022  fidcenumlemrk  7276  subhalfnqq  7787  enq0ref  7806  prarloc  7876  letrp1  9186  p1le  9187  peano2uz2  9764  uzind  9768  uzid  9952  qreccl  10058  fprodsplit1f  12426  lmodfopne  14772  wlkres  16825