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  4453  elrnrexdm  5850  uchoice  6375  tfrcl  6640  ixpsnf1o  7024  fidcenumlemrk  7278  subhalfnqq  7787  enq0ref  7806  prarloc  7876  letrp1  9186  p1le  9187  peano2uz2  9763  uzind  9767  uzid  9951  qreccl  10057  fprodsplit1f  12425  lmodfopne  14771  wlkres  16842