Theorem ancli 574

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

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  pm4.45im  585  barbari  2567  cesaro  2573  camestros  2574  calemos  2584  n0rex  3935  swopo  5045  xpdifid  5562  xpima  5576  elrnrexdm  6363  ixpsnf1o  7948  php4  8147  ssnnfi  8179  inf3lem6  8530  rankuni  8726  cardprclem  8805  nqpr  9836  letrp1  10865  p1le  10866  sup2  10979  peano2uz2  11465  uzind  11469  uzid  11702  qreccl  11808  xrsupsslem  12137  supxrunb1  12149  faclbnd4lem4  13083  cshweqdifid  13566  fprodsplit1f  14721  idghm  17675  efgred  18161  srgbinom  18545  subrgid  18782  lmodfopne  18901  m1detdiag  20403  1elcpmat  20520  phtpcer  22794  phtpcerOLD  22795  pntrlog2bndlem2  25267  wlkres  26567  clwwlksf  26915  hvpncan  27896  chsupsn  28272  ssjo  28306  elim2ifim  29364  rrhre  30065  pmeasadd  30387  bnj596  30816  bnj1209  30867  bnj996  31025  bnj1110  31050  bnj1189  31077  arg-ax  32415  bj-mo3OLD  32832  unirep  33507  rp-isfinite6  37864  clsk1indlem2  38340  ntrclsss  38361  clsneiel1  38406  monoords  39511  fsumsplit1  39804  fmul01  39812  fmuldfeqlem1  39814  fmuldfeq  39815  fmul01lt1lem1  39816  icccncfext  40100  iblspltprt  40189  stoweidlem3  40220  stoweidlem17  40234  stoweidlem19  40236  stoweidlem20  40237  stoweidlem23  40240  stirlinglem15  40305  fourierdlem16  40340  fourierdlem21  40345  fourierdlem72  40395  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  hoidmvlelem4  40812  salpreimalegt  40920  zeoALTV  41581  c0mgm  41909  c0mhm  41910  2zrngnmrid  41950  mndpsuppss  42152  linc0scn0  42212