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  2128  barbari  2189  cesaro  2195  camestros  2196  calemos  2206  swopo  4446  elrnrexdm  5838  uchoice  6361  tfrcl  6625  ixpsnf1o  7008  fidcenumlemrk  7261  subhalfnqq  7771  enq0ref  7790  prarloc  7860  letrp1  9168  p1le  9169  peano2uz2  9732  uzind  9736  uzid  9915  qreccl  10021  fprodsplit1f  12379  lmodfopne  14635  wlkres  16534