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

Theorem ancli 549
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 512 1 (𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  equsb1vOLDOLD  2510  barbariALT  2750  n0rex  4311  swopo  5477  xpdifid  6018  xpima  6032  elrnrexdm  6847  ixpsnf1o  8490  inf3lem6  9084  rankuni  9280  cardprclem  9396  nqpr  10424  letrp1  11472  p1le  11473  sup2  11585  peano2uz2  12058  uzind  12062  uzid  12246  qreccl  12356  xrsupsslem  12688  supxrunb1  12700  faclbnd4lem4  13644  cshweqdifid  14170  fprodsplit1f  15332  efgred  18803  srgbinom  19224  lmodfopne  19601  m1detdiag  21134  1elcpmat  21251  phtpcer  23526  pntrlog2bndlem2  26081  wlkres  27379  clwwlkf  27753  hvpncan  28743  chsupsn  29117  ssjo  29151  elim2ifim  30227  rrhre  31161  pmeasadd  31482  bnj596  31916  bnj1209  31967  bnj996  32126  bnj1110  32151  bnj1189  32178  swrdrevpfx  32260  pfxwlk  32267  cusgr3cyclex  32280  satefvfmla0  32562  satefvfmla1  32569  arg-ax  33661  unirep  34869  rp-isfinite6  39762  clsk1indlem2  40270  ntrclsss  40291  clsneiel1  40336  monoords  41440  fsumsplit1  41729  fmul01  41737  fmuldfeqlem1  41739  fmuldfeq  41740  fmul01lt1lem1  41741  icccncfext  42046  iblspltprt  42134  stoweidlem3  42165  stoweidlem17  42179  stoweidlem19  42181  stoweidlem20  42182  stoweidlem23  42185  stirlinglem15  42250  fourierdlem16  42285  fourierdlem21  42290  fourierdlem72  42340  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  hoidmvlelem4  42757  salpreimagelt  42863  salpreimalegt  42865  simpcntrab  43004  zeoALTV  43712  c0mgm  44108  c0mhm  44109  2zrngnmrid  44149  mndpsuppss  44347  linc0scn0  44406  eenglngeehlnm  44654
  Copyright terms: Public domain W3C validator