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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  pm4.45im  334  mo23  2128  barbari  2189  cesaro  2195  camestros  2196  calemos  2206  swopo  4451  elrnrexdm  5847  uchoice  6371  tfrcl  6635  ixpsnf1o  7018  fidcenumlemrk  7271  subhalfnqq  7781  enq0ref  7800  prarloc  7870  letrp1  9178  p1le  9179  peano2uz2  9753  uzind  9757  uzid  9936  qreccl  10042  fprodsplit1f  12401  lmodfopne  14663  wlkres  16620