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

Theorem ancli 548
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 511 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 206  df-an 396
This theorem is referenced by:  barbariALT  2660  n0rex  4350  swopo  5595  xpdifid  6166  xpima  6180  elrnrexdm  7093  ixpsnf1o  8948  inf3lem6  9648  rankuni  9878  cardprclem  9994  nqpr  11029  letrp1  12080  p1le  12081  sup2  12192  peano2uz2  12672  uzind  12676  qreccl  12975  xrsupsslem  13310  supxrunb1  13322  faclbnd4lem4  14279  cshweqdifid  14794  fsumsplit1  15715  fprodsplit1f  15958  catcone0  17658  efgred  19694  srgbinom  20162  c0mgm  20387  c0mhm  20388  lmodfopne  20772  ring2idlqus1  21198  m1detdiag  22486  1elcpmat  22604  phtpcer  24908  pntrlog2bndlem2  27498  wlkres  29471  clwwlkf  29844  hvpncan  30836  chsupsn  31210  ssjo  31244  elim2ifim  32321  rrhre  33558  pmeasadd  33881  bnj596  34313  bnj1209  34363  bnj996  34523  bnj1110  34549  bnj1189  34576  swrdrevpfx  34662  pfxwlk  34669  cusgr3cyclex  34682  satefvfmla0  34964  satefvfmla1  34971  arg-ax  35836  unirep  37122  idomnnzpownz  41535  ringexp0nn  41537  sn-sup2  41946  rp-isfinite6  42871  clsk1indlem2  43395  ntrclsss  43416  clsneiel1  43461  monoords  44602  fmul01  44891  fmuldfeqlem1  44893  fmuldfeq  44894  fmul01lt1lem1  44895  icccncfext  45198  iblspltprt  45284  stoweidlem3  45314  stoweidlem17  45328  stoweidlem19  45330  stoweidlem20  45331  stoweidlem23  45334  stirlinglem15  45399  fourierdlem16  45434  fourierdlem21  45439  fourierdlem72  45489  fourierdlem89  45506  fourierdlem90  45507  fourierdlem91  45508  hoidmvlelem4  45909  salpreimagelt  46018  salpreimalegt  46020  simpcntrab  46181  zeoALTV  46933  2zrngnmrid  47241  mndpsuppss  47358  linc0scn0  47414  eenglngeehlnm  47735  indthinc  47981  indthincALT  47982
  Copyright terms: Public domain W3C validator