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

Theorem ancli 534
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 19 . 2  |-  ( ph  ->  ph )
2 ancli.1 . 2  |-  ( ph  ->  ps )
31, 2jca 518 1  |-  ( ph  ->  ( ph  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  pm4.45im  545  mo  2165  2mo  2221  barbari  2244  cesaro  2250  camestros  2251  calemos  2261  swopo  4324  oelim2  6593  ixpsnf1o  6856  php4  7048  ssnnfi  7082  inf3lem6  7334  rankuni  7535  cardprclem  7612  nqpr  8638  letrp1  9598  p1le  9599  sup2  9710  peano2uz2  10099  uzind  10103  uzid  10242  qreccl  10336  xrsupsslem  10625  supxrunb1  10638  faclbnd4lem4  11309  idghm  14698  efgred  15057  subrgid  15547  phtpcer  18493  pntrlog2bndlem2  20727  hvpncan  21618  chsupsn  21992  ssjo  22026  elim2ifim  23153  xpima  23202  arg-ax  24855  unirep  26349  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  stoweidlem17  27766  stoweidlem22  27771  stoweidlem23  27772  stoweidlem35  27784  stoweidlem55  27804  stoweidlem59  27808  stirlinglem4  27826  bnj596  28775  bnj1209  28829  bnj996  28987  bnj1110  29012  bnj1189  29039
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 177  df-an 360
  Copyright terms: Public domain W3C validator