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

Theorem ancli 551
Description: Deduction conjoining antecedent to left of consequent. (Contributed by NM, 12-Aug-1993.)
Hypothesis
Ref Expression
ancli.1
Assertion
Ref Expression
ancli

Proof of Theorem ancli
StepHypRef Expression
1 id 22 . 2
2 ancli.1 . 2
31, 2jca 532 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  pm4.45im  562  mo3OLD  2324  barbari  2400  cesaro  2406  camestros  2407  calemos  2417  swopo  4815  xpdifid  5440  xpima  5454  elrnrexdm  6035  ixpsnf1o  7529  php4  7724  ssnnfi  7759  inf3lem6  8071  rankuni  8302  cardprclem  8381  nqpr  9413  letrp1  10409  p1le  10410  sup2  10524  peano2uz2  10975  uzind  10979  uzid  11124  qreccl  11231  xrsupsslem  11527  supxrunb1  11540  faclbnd4lem4  12374  cshweqdifid  12788  idghm  16282  efgred  16766  srgbinom  17196  subrgid  17431  m1detdiag  19099  1elcpmat  19216  phtpcer  21495  pntrlog2bndlem2  23763  wlkon  24533  trlon  24542  pthon  24577  spthon  24584  constr3lem6  24649  clwwlkf  24794  hvpncan  25956  chsupsn  26331  ssjo  26365  elim2ifim  27423  rrhre  27999  arg-ax  29881  unirep  30203  monoords  31496  fsumsplit1  31573  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fprodsplit1f  31593  icccncfext  31690  iblspltprt  31772  stoweidlem3  31785  stoweidlem17  31799  stoweidlem19  31801  stoweidlem20  31802  stoweidlem23  31805  stirlinglem15  31870  fourierdlem16  31905  fourierdlem21  31910  fourierdlem72  31961  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  c0mgm  32715  c0mhm  32716  2zrngnmrid  32756  mndpsuppss  32964  linc0scn0  33024  bnj596  33803  bnj1209  33855  bnj996  34013  bnj1110  34038  bnj1189  34065  rp-isfinite6  37744
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
  Copyright terms: Public domain W3C validator