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  7782  enq0ref  7801  prarloc  7871  letrp1  9181  p1le  9182  peano2uz2  9758  uzind  9762  uzid  9946  qreccl  10052  fprodsplit1f  12420  lmodfopne  14747  wlkres  16786