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  2124  barbari  2185  cesaro  2191  camestros  2192  calemos  2202  swopo  4432  elrnrexdm  5821  uchoice  6344  tfrcl  6608  ixpsnf1o  6984  fidcenumlemrk  7237  subhalfnqq  7745  enq0ref  7764  prarloc  7834  letrp1  9139  p1le  9140  peano2uz2  9703  uzind  9707  uzid  9886  qreccl  9992  fprodsplit1f  12345  lmodfopne  14600  wlkres  16500