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  2099  barbari  2160  cesaro  2166  camestros  2167  calemos  2177  swopo  4374  elrnrexdm  5747  uchoice  6253  tfrcl  6480  ixpsnf1o  6853  fidcenumlemrk  7089  subhalfnqq  7569  enq0ref  7588  prarloc  7658  letrp1  8963  p1le  8964  peano2uz2  9522  uzind  9526  uzid  9704  qreccl  9805  fprodsplit1f  12111  lmodfopne  14255