Theorem ancli 553

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  pm4.45im  564  barbari  2365  cesaro  2371  camestros  2372  calemos  2382  swopo  4780  xpdifid  5280  xpima  5294  elrnrexdm  6037  ixpsnf1o  7566  php4  7761  ssnnfi  7793  inf3lem6  8140  rankuni  8335  cardprclem  8414  nqpr  9439  letrp1  10447  p1le  10448  sup2  10565  peano2uz2  11023  uzind  11027  uzid  11173  qreccl  11284  xrsupsslem  11592  supxrunb1  11605  faclbnd4lem4  12480  cshweqdifid  12907  fprodsplit1f  14029  idghm  16883  efgred  17383  srgbinom  17763  subrgid  17995  m1detdiag  19606  1elcpmat  19723  phtpcer  22010  pntrlog2bndlem2  24400  wlkon  25244  trlon  25253  pthon  25288  spthon  25295  constr3lem6  25360  clwwlkf  25505  hvpncan  26675  chsupsn  27049  ssjo  27083  elim2ifim  28149  rrhre  28818  pmeasadd  29151  bnj596  29549  bnj1209  29601  bnj996  29759  bnj1110  29784  bnj1189  29811  arg-ax  31066  bj-mo3OLD  31402  unirep  31950  rp-isfinite6  36080  monoords  37353  fsumsplit1  37471  fmul01  37475  fmuldfeqlem1  37477  fmuldfeq  37478  fmul01lt1lem1  37479  icccncfext  37582  iblspltprt  37667  stoweidlem3  37680  stoweidlem17  37694  stoweidlem19  37696  stoweidlem20  37697  stoweidlem23  37700  stirlinglem15  37767  fourierdlem16  37802  fourierdlem21  37807  fourierdlem72  37859  fourierdlem89  37876  fourierdlem90  37877  fourierdlem91  37878  zeoALTV  38508  c0mgm  39095  c0mhm  39096  2zrngnmrid  39136  mndpsuppss  39344  linc0scn0  39404