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  2083  barbari  2144  cesaro  2150  camestros  2151  calemos  2161  swopo  4337  elrnrexdm  5697  uchoice  6190  tfrcl  6417  ixpsnf1o  6790  fidcenumlemrk  7013  subhalfnqq  7474  enq0ref  7493  prarloc  7563  letrp1  8867  p1le  8868  peano2uz2  9424  uzind  9428  uzid  9606  qreccl  9707  fprodsplit1f  11777  lmodfopne  13822