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

Theorem ancli 573
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 554 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 197  df-an 386
This theorem is referenced by:  pm4.45im  584  barbari  2566  cesaro  2572  camestros  2573  calemos  2583  n0rex  3916  swopo  5010  xpdifid  5526  xpima  5540  elrnrexdm  6324  ixpsnf1o  7900  php4  8099  ssnnfi  8131  inf3lem6  8482  rankuni  8678  cardprclem  8757  nqpr  9788  letrp1  10817  p1le  10818  sup2  10931  peano2uz2  11417  uzind  11421  uzid  11654  qreccl  11760  xrsupsslem  12088  supxrunb1  12100  faclbnd4lem4  13031  cshweqdifid  13511  fprodsplit1f  14657  idghm  17607  efgred  18093  srgbinom  18477  subrgid  18714  lmodfopne  18833  m1detdiag  20335  1elcpmat  20452  phtpcer  22717  phtpcerOLD  22718  pntrlog2bndlem2  25184  wlkres  26453  clwwlksf  26798  hvpncan  27766  chsupsn  28142  ssjo  28176  elim2ifim  29234  rrhre  29871  pmeasadd  30192  bnj596  30559  bnj1209  30610  bnj996  30768  bnj1110  30793  bnj1189  30820  arg-ax  32092  bj-mo3OLD  32512  unirep  33174  rp-isfinite6  37380  clsk1indlem2  37857  ntrclsss  37878  clsneiel1  37923  monoords  39006  fsumsplit1  39236  fmul01  39244  fmuldfeqlem1  39246  fmuldfeq  39247  fmul01lt1lem1  39248  icccncfext  39431  iblspltprt  39522  stoweidlem3  39553  stoweidlem17  39567  stoweidlem19  39569  stoweidlem20  39570  stoweidlem23  39573  stirlinglem15  39638  fourierdlem16  39673  fourierdlem21  39678  fourierdlem72  39728  fourierdlem89  39745  fourierdlem90  39746  fourierdlem91  39747  hoidmvlelem4  40145  salpreimalegt  40253  zeoALTV  40906  c0mgm  41223  c0mhm  41224  2zrngnmrid  41264  mndpsuppss  41466  linc0scn0  41526
  Copyright terms: Public domain W3C validator