Theorem ancli 321

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 304	1 |- ( ph -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  pm4.45im  332  mo23  2060  barbari  2121  cesaro  2127  camestros  2128  calemos  2138  swopo  4291  elrnrexdm  5635  tfrcl  6343  ixpsnf1o  6714  fidcenumlemrk  6931  subhalfnqq  7376  enq0ref  7395  prarloc  7465  letrp1  8764  p1le  8765  peano2uz2  9319  uzind  9323  uzid  9501  qreccl  9601  fprodsplit1f  11597