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  2121  barbari  2182  cesaro  2188  camestros  2189  calemos  2199  swopo  4403  elrnrexdm  5786  uchoice  6300  tfrcl  6530  ixpsnf1o  6905  fidcenumlemrk  7153  subhalfnqq  7634  enq0ref  7653  prarloc  7723  letrp1  9028  p1le  9029  peano2uz2  9587  uzind  9591  uzid  9770  qreccl  9876  fprodsplit1f  12213  lmodfopne  14359  wlkres  16249