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  2178  2mo  2234  barbari  2257  cesaro  2263  camestros  2264  calemos  2274  swopo  4340  oelim2  6609  ixpsnf1o  6872  php4  7064  ssnnfi  7098  inf3lem6  7350  rankuni  7551  cardprclem  7628  nqpr  8654  letrp1  9614  p1le  9615  sup2  9726  peano2uz2  10115  uzind  10119  uzid  10258  qreccl  10352  xrsupsslem  10641  supxrunb1  10654  faclbnd4lem4  11325  idghm  14714  efgred  15073  subrgid  15563  phtpcer  18509  pntrlog2bndlem2  20743  hvpncan  21634  chsupsn  22008  ssjo  22042  elim2ifim  23169  xpima  23217  arg-ax  24927  unirep  26452  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  stoweidlem17  27869  stoweidlem22  27874  stoweidlem23  27875  stoweidlem35  27887  stoweidlem55  27907  stoweidlem59  27911  stirlinglem4  27929  trlon  28339  pthon  28361  constr3lem6  28395  bnj596  29091  bnj1209  29145  bnj996  29303  bnj1110  29328  bnj1189  29355
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