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  2096  barbari  2157  cesaro  2163  camestros  2164  calemos  2174  swopo  4357  elrnrexdm  5726  uchoice  6230  tfrcl  6457  ixpsnf1o  6830  fidcenumlemrk  7063  subhalfnqq  7534  enq0ref  7553  prarloc  7623  letrp1  8928  p1le  8929  peano2uz2  9487  uzind  9491  uzid  9669  qreccl  9770  fprodsplit1f  11989  lmodfopne  14132