Theorem ancli 558

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 539	1 |- ( ph -> ( ph /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  pm4.45im  569  barbari  2407  cesaro  2413  camestros  2414  calemos  2424  swopo  4787  xpdifid  5287  xpima  5301  elrnrexdm  6054  ixpsnf1o  7593  php4  7790  ssnnfi  7822  inf3lem6  8169  rankuni  8365  cardprclem  8444  nqpr  9470  letrp1  10480  p1le  10481  sup2  10598  peano2uz2  11057  uzind  11061  uzid  11207  qreccl  11318  xrsupsslem  11626  supxrunb1  11639  faclbnd4lem4  12519  cshweqdifid  12962  fprodsplit1f  14099  idghm  16953  efgred  17453  srgbinom  17833  subrgid  18065  m1detdiag  19677  1elcpmat  19794  phtpcer  22081  pntrlog2bndlem2  24472  wlkon  25317  trlon  25326  pthon  25361  spthon  25368  constr3lem6  25433  clwwlkf  25578  hvpncan  26748  chsupsn  27122  ssjo  27156  elim2ifim  28217  rrhre  28876  pmeasadd  29208  bnj596  29606  bnj1209  29658  bnj996  29816  bnj1110  29841  bnj1189  29868  arg-ax  31126  bj-mo3OLD  31493  unirep  32085  rp-isfinite6  36209  monoords  37589  fsumsplit1  37736  fmul01  37744  fmuldfeqlem1  37746  fmuldfeq  37747  fmul01lt1lem1  37748  icccncfext  37851  iblspltprt  37936  stoweidlem3  37964  stoweidlem17  37978  stoweidlem19  37980  stoweidlem20  37981  stoweidlem23  37984  stirlinglem15  38051  fourierdlem16  38086  fourierdlem21  38091  fourierdlem72  38143  fourierdlem89  38160  fourierdlem90  38161  fourierdlem91  38162  hoidmvlelem4  38527  zeoALTV  38934  n0rex  39125  c0mgm  40278  c0mhm  40279  2zrngnmrid  40319  mndpsuppss  40525  linc0scn0  40585