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

Theorem ancli 540
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 503 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  pm4.45im  849  barbariALT  2734  cesaroOLD  2745  camestrosOLD  2747  calemosOLD  2764  n0rex  4136  swopo  5242  xpdifid  5773  xpima  5787  elrnrexdm  6581  ixpsnf1o  8181  php4  8382  ssnnfi  8414  inf3lem6  8773  rankuni  8969  cardprclem  9084  nqpr  10117  letrp1  11146  p1le  11147  sup2  11260  peano2uz2  11727  uzind  11731  uzid  11915  qreccl  12023  xrsupsslem  12351  supxrunb1  12363  faclbnd4lem4  13299  cshweqdifid  13786  fprodsplit1f  14937  idghm  17873  efgred  18358  srgbinom  18743  subrgid  18982  lmodfopne  19101  m1detdiag  20610  1elcpmat  20729  phtpcer  23003  pntrlog2bndlem2  25477  wlkres  26791  clwwlkf  27192  hvpncan  28220  chsupsn  28596  ssjo  28630  elim2ifim  29685  rrhre  30386  pmeasadd  30708  bnj596  31134  bnj1209  31185  bnj996  31343  bnj1110  31368  bnj1189  31395  arg-ax  32727  bj-mo3OLD  33140  unirep  33814  rp-isfinite6  38358  clsk1indlem2  38834  ntrclsss  38855  clsneiel1  38900  monoords  39986  fsumsplit1  40278  fmul01  40286  fmuldfeqlem1  40288  fmuldfeq  40289  fmul01lt1lem1  40290  icccncfext  40574  iblspltprt  40662  stoweidlem3  40693  stoweidlem17  40707  stoweidlem19  40709  stoweidlem20  40710  stoweidlem23  40713  stirlinglem15  40778  fourierdlem16  40813  fourierdlem21  40818  fourierdlem72  40868  fourierdlem89  40885  fourierdlem90  40886  fourierdlem91  40887  hoidmvlelem4  41288  salpreimalegt  41396  zeoALTV  42150  c0mgm  42471  c0mhm  42472  2zrngnmrid  42512  mndpsuppss  42714  linc0scn0  42774
  Copyright terms: Public domain W3C validator