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  2119  barbari  2180  cesaro  2186  camestros  2187  calemos  2197  swopo  4398  elrnrexdm  5779  uchoice  6292  tfrcl  6521  ixpsnf1o  6896  fidcenumlemrk  7137  subhalfnqq  7617  enq0ref  7636  prarloc  7706  letrp1  9011  p1le  9012  peano2uz2  9570  uzind  9574  uzid  9753  qreccl  9854  fprodsplit1f  12166  lmodfopne  14311  wlkres  16149