MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancld Unicode version

Theorem ancld 553
Description: Deduction conjoining antecedent to left of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)
Hypothesis
Ref Expression
ancld.1
Assertion
Ref Expression
ancld

Proof of Theorem ancld
StepHypRef Expression
1 idd 24 . 2
2 ancld.1 . 2
31, 2jcad 533 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  mopick2  2362  2eu6  2383  cgsexg  3142  cgsex2g  3143  cgsex4g  3144  reximdva0  3796  difsn  4164  preq12b  4206  ordtr2  4927  elres  5314  relssres  5316  elunirn  6163  fnoprabg  6403  tz7.49  7129  omord  7236  ficard  8961  fpwwe2lem12  9040  1idpr  9428  xrsupsslem  11527  xrinfmsslem  11528  fzospliti  11857  sqrt2irr  13982  algcvga  14208  prmind2  14228  infpn2  14431  grpinveu  16084  1stcrest  19954  fgss2  20375  fgcl  20379  filufint  20421  metrest  21027  reconnlem2  21332  plydivex  22693  ftalem3  23348  chtub  23487  2sqlem10  23649  dchrisum0flb  23695  pntpbnd1  23771  2pthfrgrarn2  25010  grpoidinvlem3  25208  grpoinveu  25224  ifbieq12d2  27420  elim2ifim  27423  iocinif  27592  tpr2rico  27894  dfon2lem8  29222  dftrpred3g  29316  nofulllem5  29466  voliunnfl  30058  nn0prpwlem  30140  ax6e2eq  33330  bnj168  33785  dalem20  35417  elpaddn0  35524  cdleme25a  36079  cdleme29ex  36100  cdlemefr29exN  36128  dibglbN  36893  dihlsscpre  36961  lcfl7N  37228  mapdh9a  37517  mapdh9aOLDN  37518  hdmap11lem2  37572
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 185  df-an 371
  Copyright terms: Public domain W3C validator