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  2321  moOLD  2327  2moOLDOLD  2384  barbari  2410  cesaro  2416  camestros  2417  calemos  2427  swopo  4810  xpdifid  5433  xpima  5447  elrnrexdm  6023  oelim2  7241  ixpsnf1o  7506  php4  7701  ssnnfi  7736  inf3lem6  8046  rankuni  8277  cardprclem  8356  nqpr  9388  letrp1  10380  p1le  10381  sup2  10495  peano2uz2  10944  uzind  10948  uzid  11092  qreccl  11198  xrsupsslem  11494  supxrunb1  11507  faclbnd4lem4  12338  hashf1rn  12389  cshweqdifid  12747  idghm  16077  efgred  16562  srgbinom  16984  subrgid  17214  m1detdiag  18866  1elcpmat  18983  phtpcer  21230  pntrlog2bndlem2  23491  wlkon  24209  trlon  24218  pthon  24253  spthon  24260  constr3lem6  24325  clwwlkf  24470  hvpncan  25632  chsupsn  26007  ssjo  26041  elim2ifim  27097  rrhre  27635  arg-ax  29458  wl-sbal2  29591  unirep  29806  monoords  31073  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  icccncfext  31226  iblspltprt  31291  stoweidlem3  31303  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem23  31323  stirlinglem15  31388  fourierdlem21  31428  fourierdlem72  31479  mndpsuppss  32037  linc0scn0  32097  bnj596  32882  bnj1209  32934  bnj996  33092  bnj1110  33117  bnj1189  33144