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

Theorem ancld 540
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 502 1 (𝜑 → (𝜓 → (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  equvinvOLD  2116  mo2v  2625  mopick2  2689  2eu6  2707  cgsexg  3390  cgsex2g  3391  cgsex4g  3392  reximdva0  4080  difsn  4464  preq12b  4513  elres  5576  relssres  5578  ordtr2  5911  elunirn  6652  fnoprabg  6908  tz7.49  7693  omord  7802  ficard  9589  fpwwe2lem12  9665  1idpr  10053  xrsupsslem  12342  xrinfmsslem  12343  fzospliti  12708  sqrt2irr  15185  algcvga  15500  prmind2  15605  infpn2  15824  grpinveu  17664  1stcrest  21477  fgss2  21898  fgcl  21902  filufint  21944  metrest  22549  reconnlem2  22850  plydivex  24272  ftalem3  25022  chtub  25158  lgsqrmodndvds  25299  2sqlem10  25374  dchrisum0flb  25420  pntpbnd1  25496  clwwlkn1loopb  27199  2pthfrgrrn2  27465  grpoidinvlem3  27700  grpoinveu  27713  elim2ifim  29702  iocinif  29883  tpr2rico  30298  bnj168  31136  dfon2lem8  32031  dftrpred3g  32069  nolesgn2o  32161  nosupbnd1lem4  32194  nn0prpwlem  32654  voliunnfl  33786  dalem20  35501  elpaddn0  35608  cdleme25a  36162  cdleme29ex  36183  cdlemefr29exN  36211  dibglbN  36976  dihlsscpre  37044  lcfl7N  37311  mapdh9a  37599  mapdh9aOLDN  37600  hdmap11lem2  37652  ax6e2eq  39298  eliin2f  39808
  Copyright terms: Public domain W3C validator