Theorem ancli 549

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

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  pm4.45im  560  mo3OLD  2325  barbari  2397  cesaro  2403  camestros  2404  calemos  2414  swopo  4799  xpdifid  5420  xpima  5434  elrnrexdm  6011  ixpsnf1o  7502  php4  7697  ssnnfi  7732  inf3lem6  8041  rankuni  8272  cardprclem  8351  nqpr  9381  letrp1  10380  p1le  10381  sup2  10494  peano2uz2  10946  uzind  10950  uzid  11096  qreccl  11203  xrsupsslem  11501  supxrunb1  11514  faclbnd4lem4  12359  cshweqdifid  12782  idghm  16484  efgred  16968  srgbinom  17394  subrgid  17629  m1detdiag  19269  1elcpmat  19386  phtpcer  21664  pntrlog2bndlem2  23964  wlkon  24738  trlon  24747  pthon  24782  spthon  24789  constr3lem6  24854  clwwlkf  24999  hvpncan  26157  chsupsn  26532  ssjo  26566  elim2ifim  27632  rrhre  28236  arg-ax  30112  unirep  30446  monoords  31738  fsumsplit1  31815  fmul01  31816  fmuldfeqlem1  31818  fmuldfeq  31819  fmul01lt1lem1  31820  fprodsplit1f  31835  icccncfext  31932  iblspltprt  32014  stoweidlem3  32027  stoweidlem17  32041  stoweidlem19  32043  stoweidlem20  32044  stoweidlem23  32047  stirlinglem15  32112  fourierdlem16  32147  fourierdlem21  32152  fourierdlem72  32203  fourierdlem89  32220  fourierdlem90  32221  fourierdlem91  32222  zeoALTV  32584  c0mgm  32988  c0mhm  32989  2zrngnmrid  33029  mndpsuppss  33237  linc0scn0  33297  bnj596  34223  bnj1209  34275  bnj996  34433  bnj1110  34458  bnj1189  34485  rp-isfinite6  38176