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  2067  barbari  2128  cesaro  2134  camestros  2135  calemos  2145  swopo  4308  elrnrexdm  5657  tfrcl  6367  ixpsnf1o  6738  fidcenumlemrk  6955  subhalfnqq  7415  enq0ref  7434  prarloc  7504  letrp1  8807  p1le  8808  peano2uz2  9362  uzind  9366  uzid  9544  qreccl  9644  fprodsplit1f  11644  lmodfopne  13421