Theorem ancli 551

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 22	. 2 |- ( ph -> ph )
2		ancli.1	. 2 |- ( ph -> ps )
3	1, 2	jca 532	1 |- ( ph -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371

This theorem is referenced by:  pm4.45im  562  mo3OLD  2306  moOLD  2312  2moOLDOLD  2369  barbari  2395  cesaro  2401  camestros  2402  calemos  2412  swopo  4752  xpdifid  5367  xpima  5381  elrnrexdm  5949  oelim2  7137  ixpsnf1o  7406  php4  7601  ssnnfi  7636  inf3lem6  7943  rankuni  8174  cardprclem  8253  nqpr  9287  letrp1  10275  p1le  10276  sup2  10390  peano2uz2  10833  uzind  10837  uzid  10979  qreccl  11077  xrsupsslem  11373  supxrunb1  11386  faclbnd4lem4  12182  hashf1rn  12233  cshweqdifid  12565  idghm  15873  efgred  16358  srgbinom  16758  subrgid  16982  m1detdiag  18528  phtpcer  20692  pntrlog2bndlem2  22953  wlkon  23574  trlon  23584  pthon  23619  spthon  23626  constr3lem6  23680  hvpncan  24586  chsupsn  24961  ssjo  24995  elim2ifim  26051  rrhre  26585  arg-ax  28399  wl-sbal2  28531  unirep  28747  fmuldfeqlem1  29904  fmuldfeq  29905  fmul01lt1lem1  29906  stoweidlem3  29939  stoweidlem17  29953  stoweidlem19  29955  stoweidlem20  29956  stoweidlem23  29959  stirlinglem15  30024  clwwlkf  30597  mndpsuppss  30925  linc0scn0  31067  1elcpmat  31181  bnj596  32041  bnj1209  32093  bnj996  32251  bnj1110  32276  bnj1189  32303