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  2297  moOLD  2303  2mo  2357  2moOLD  2358  2moOLDOLD  2359  barbari  2384  cesaro  2390  camestros  2391  calemos  2401  swopo  4646  xpdifid  5261  xpima  5275  elrnrexdm  5842  oelim2  7026  ixpsnf1o  7295  php4  7490  ssnnfi  7524  inf3lem6  7831  rankuni  8062  cardprclem  8141  nqpr  9175  letrp1  10163  p1le  10164  sup2  10278  peano2uz2  10721  uzind  10725  uzid  10867  qreccl  10965  xrsupsslem  11261  supxrunb1  11274  faclbnd4lem4  12064  hashf1rn  12115  cshweqdifid  12446  idghm  15753  efgred  16236  srgbinom  16631  subrgid  16845  phtpcer  20542  pntrlog2bndlem2  22802  wlkon  23380  trlon  23390  pthon  23425  spthon  23432  constr3lem6  23486  hvpncan  24392  chsupsn  24767  ssjo  24801  elim2ifim  25858  rrhre  26399  arg-ax  28214  wl-sbal2  28341  wl-lem-mo-recur  28346  wl-lem-moreduce  28347  unirep  28559  fmuldfeqlem1  29716  fmuldfeq  29717  fmul01lt1lem1  29718  stoweidlem3  29751  stoweidlem17  29765  stoweidlem19  29767  stoweidlem20  29768  stoweidlem23  29771  stirlinglem15  29836  clwwlkf  30409  mndpsuppss  30735  m1detdiag  30823  linc0scn0  30846  bnj596  31625  bnj1209  31677  bnj996  31835  bnj1110  31860  bnj1189  31887