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  2040  barbari  2101  cesaro  2107  camestros  2108  calemos  2118  swopo  4228  elrnrexdm  5559  tfrcl  6261  ixpsnf1o  6630  fidcenumlemrk  6842  subhalfnqq  7222  enq0ref  7241  prarloc  7311  letrp1  8606  p1le  8607  peano2uz2  9158  uzind  9162  uzid  9340  qreccl  9434