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  2121  barbari  2182  cesaro  2188  camestros  2189  calemos  2199  swopo  4403  elrnrexdm  5786  uchoice  6299  tfrcl  6529  ixpsnf1o  6904  fidcenumlemrk  7152  subhalfnqq  7633  enq0ref  7652  prarloc  7722  letrp1  9027  p1le  9028  peano2uz2  9586  uzind  9590  uzid  9769  qreccl  9875  fprodsplit1f  12194  lmodfopne  14339  wlkres  16229