MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancli Structured version   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  2302  2mo  2358  barbari  2381  cesaro  2387  camestros  2388  calemos  2398  swopo  4505  xpima  5305  elrnrexdm  5866  oelim2  6830  ixpsnf1o  7094  php4  7286  ssnnfi  7320  inf3lem6  7580  rankuni  7781  cardprclem  7858  nqpr  8883  letrp1  9844  p1le  9845  sup2  9956  peano2uz2  10349  uzind  10353  uzid  10492  qreccl  10586  xrsupsslem  10877  supxrunb1  10890  faclbnd4lem4  11579  hashf1rn  11628  idghm  15013  efgred  15372  subrgid  15862  phtpcer  19012  pntrlog2bndlem2  21264  wlkon  21522  trlon  21532  pthon  21567  spthon  21574  constr3lem6  21628  hvpncan  22533  chsupsn  22907  ssjo  22941  elim2ifim  23998  rrhre  24379  arg-ax  26158  unirep  26405  fmuldfeqlem1  27679  fmuldfeq  27680  fmul01lt1lem1  27681  stoweidlem3  27719  stoweidlem17  27733  stoweidlem19  27735  stoweidlem20  27736  stoweidlem23  27739  stirlinglem15  27804  2cshw2lem1  28218  bnj596  29051  bnj1209  29105  bnj996  29263  bnj1110  29288  bnj1189  29315
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