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

Theorem ancld 554
 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 516 1 (𝜑 → (𝜓 → (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  dfmoeu  2594  mopick2  2699  2eu6  2719  cgsexg  3485  cgsex2g  3486  cgsex4g  3487  cgsex4gOLD  3488  ss2abdv  3993  reximdva0  4268  difsn  4694  preq12b  4744  elinxp  5860  ssrnres  6006  ordtr2  6210  elunirn  6998  fnoprabg  7264  tz7.49  8082  omord  8195  ficard  9994  fpwwe2lem11  10070  1idpr  10458  xrsupsslem  12708  xrinfmsslem  12709  fzospliti  13084  sqrt2irr  15614  algcvga  15933  prmind2  16039  infpn2  16259  grpinveu  18151  1stcrest  22099  fgss2  22520  fgcl  22524  filufint  22566  metrest  23172  reconnlem2  23473  plydivex  24937  ftalem3  25704  chtub  25840  lgsqrmodndvds  25981  2sqlem10  26056  dchrisum0flb  26138  pntpbnd1  26214  clwwlkn1loopb  27872  2pthfrgrrn2  28112  grpoidinvlem3  28333  grpoinveu  28346  elim2ifim  30356  iocinif  30574  qsxpid  31027  tpr2rico  31331  bnj168  32176  dfon2lem8  33218  dftrpred3g  33255  nolesgn2o  33361  nosupbnd1lem4  33401  noinfbnd1lem4  33416  noetalem1  33431  nn0prpwlem  33930  bj-opelidres  34727  difunieq  34942  voliunnfl  35252  dalem20  37140  elpaddn0  37247  cdleme25a  37800  cdleme29ex  37821  cdlemefr29exN  37849  dibglbN  38613  dihlsscpre  38681  lcfl7N  38948  mapdh9a  39236  mapdh9aOLDN  39237  hdmap11lem2  39289  rtprmirr  39673  sqrtcval  40512  ax6e2eq  41434  eliin2f  41911  itschlc0xyqsol1  45346
 Copyright terms: Public domain W3C validator