Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancli Structured version   Visualization version   GIF 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 514 1 (𝜑 → (𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398 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 209  df-an 399 This theorem is referenced by:  equsb1vOLDOLD  2511  barbariALT  2751  n0rex  4312  swopo  5477  xpdifid  6018  xpima  6032  elrnrexdm  6848  ixpsnf1o  8494  inf3lem6  9088  rankuni  9284  cardprclem  9400  nqpr  10428  letrp1  11476  p1le  11477  sup2  11589  peano2uz2  12062  uzind  12066  uzid  12250  qreccl  12360  xrsupsslem  12692  supxrunb1  12704  faclbnd4lem4  13648  cshweqdifid  14174  fprodsplit1f  15336  efgred  18866  srgbinom  19287  lmodfopne  19664  m1detdiag  21198  1elcpmat  21315  phtpcer  23591  pntrlog2bndlem2  26146  wlkres  27444  clwwlkf  27818  hvpncan  28808  chsupsn  29182  ssjo  29216  elim2ifim  30292  rrhre  31250  pmeasadd  31571  bnj596  32005  bnj1209  32056  bnj996  32216  bnj1110  32242  bnj1189  32269  swrdrevpfx  32351  pfxwlk  32358  cusgr3cyclex  32371  satefvfmla0  32653  satefvfmla1  32660  arg-ax  33752  unirep  34975  rp-isfinite6  39869  clsk1indlem2  40377  ntrclsss  40398  clsneiel1  40443  monoords  41548  fsumsplit1  41837  fmul01  41845  fmuldfeqlem1  41847  fmuldfeq  41848  fmul01lt1lem1  41849  icccncfext  42154  iblspltprt  42242  stoweidlem3  42273  stoweidlem17  42287  stoweidlem19  42289  stoweidlem20  42290  stoweidlem23  42293  stirlinglem15  42358  fourierdlem16  42393  fourierdlem21  42398  fourierdlem72  42448  fourierdlem89  42465  fourierdlem90  42466  fourierdlem91  42467  hoidmvlelem4  42865  salpreimagelt  42971  salpreimalegt  42973  simpcntrab  43112  zeoALTV  43820  c0mgm  44165  c0mhm  44166  2zrngnmrid  44206  mndpsuppss  44404  linc0scn0  44463  eenglngeehlnm  44711
 Copyright terms: Public domain W3C validator