Theorem ancli 316

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

Syntax hints:   -> wi 4   /\ wa 102

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

This theorem is referenced by:  pm4.45im  327  mo23  1982  barbari  2043  cesaro  2049  camestros  2050  calemos  2060  swopo  4061  elrnrexdm  5327  subhalfnqq  6604  enq0ref  6623  prarloc  6693  letrp1  7926  p1le  7927  peano2uz2  8454  uzind  8458  uzid  8633  qreccl  8727