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

Theorem ancld 575
 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 555 1 (𝜑 → (𝜓 → (𝜓𝜒)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  equvinv  1956  equvinivOLD  1958  mo2v  2476  mopick2  2539  2eu6  2557  cgsexg  3224  cgsex2g  3225  cgsex4g  3226  reximdva0  3909  difsn  4297  preq12b  4350  elres  5394  relssres  5396  ordtr2  5727  elunirn  6463  fnoprabg  6714  tz7.49  7485  omord  7593  ficard  9331  fpwwe2lem12  9407  1idpr  9795  xrsupsslem  12080  xrinfmsslem  12081  fzospliti  12441  sqrt2irr  14903  algcvga  15216  prmind2  15322  infpn2  15541  grpinveu  17377  1stcrest  21166  fgss2  21588  fgcl  21592  filufint  21634  metrest  22239  reconnlem2  22538  plydivex  23956  ftalem3  24701  chtub  24837  lgsqrmodndvds  24978  2sqlem10  25053  dchrisum0flb  25099  pntpbnd1  25175  2pthfrgrrn2  27011  grpoidinvlem3  27209  grpoinveu  27222  elim2ifim  29211  iocinif  29387  tpr2rico  29740  bnj168  30506  dfon2lem8  31396  dftrpred3g  31434  nn0prpwlem  31959  voliunnfl  33085  dalem20  34459  elpaddn0  34566  cdleme25a  35121  cdleme29ex  35142  cdlemefr29exN  35170  dibglbN  35935  dihlsscpre  36003  lcfl7N  36270  mapdh9a  36559  mapdh9aOLDN  36560  hdmap11lem2  36614  ax6e2eq  38255  eliin2f  38772
 Copyright terms: Public domain W3C validator