MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancli Unicode version

Theorem ancli 535
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
StepHypRef Expression
1 id 20 . 2  |-  ( ph  ->  ph )
2 ancli.1 . 2  |-  ( ph  ->  ps )
31, 2jca 519 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  pm4.45im  546  mo  2261  2mo  2317  barbari  2340  cesaro  2346  camestros  2347  calemos  2357  swopo  4455  xpima  5254  elrnrexdm  5814  oelim2  6775  ixpsnf1o  7039  php4  7231  ssnnfi  7265  inf3lem6  7522  rankuni  7723  cardprclem  7800  nqpr  8825  letrp1  9785  p1le  9786  sup2  9897  peano2uz2  10290  uzind  10294  uzid  10433  qreccl  10527  xrsupsslem  10818  supxrunb1  10831  faclbnd4lem4  11515  hashf1rn  11564  idghm  14949  efgred  15308  subrgid  15798  phtpcer  18892  pntrlog2bndlem2  21140  wlkon  21395  trlon  21405  pthon  21430  constr3lem6  21485  hvpncan  22390  chsupsn  22764  ssjo  22798  elim2ifim  23851  rrhre  24184  arg-ax  25881  unirep  26106  fmuldfeqlem1  27381  fmuldfeq  27382  fmul01lt1lem1  27383  stoweidlem3  27421  stoweidlem17  27435  stoweidlem19  27437  stoweidlem20  27438  stoweidlem23  27441  stirlinglem15  27506  bnj596  28453  bnj1209  28507  bnj996  28665  bnj1110  28690  bnj1189  28717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator