MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ancld Structured version   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  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ancld  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )

Proof of Theorem ancld
StepHypRef Expression
1 idd 24 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 533 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  mopick2  2370  2eu6  2393  cgsexg  3146  cgsex2g  3147  cgsex4g  3148  reximdva0  3796  difsn  4161  preq12b  4202  ordtr2  4922  elres  5309  relssres  5311  elunirn  6152  fnoprabg  6388  tz7.49  7111  omord  7218  ficard  8941  fpwwe2lem12  9020  1idpr  9408  xrsupsslem  11499  xrinfmsslem  11500  fzospliti  11826  sqrt2irr  13846  algcvga  14070  prmind2  14090  infpn2  14293  grpinveu  15898  1stcrest  19760  fgss2  20202  fgcl  20206  filufint  20248  metrest  20854  reconnlem2  21159  plydivex  22519  ftalem3  23173  chtub  23312  2sqlem10  23474  dchrisum0flb  23520  pntpbnd1  23596  2pthfrgrarn2  24783  grpoidinvlem3  24981  grpoinveu  24997  ifbieq12d2  27191  elim2ifim  27194  iocinif  27357  tpr2rico  27645  dfon2lem8  29075  dftrpred3g  29169  nofulllem5  29319  voliunnfl  29911  nn0prpwlem  29993  ax6e2eq  32627  bnj168  33082  dalem20  34706  elpaddn0  34813  cdleme25a  35366  cdleme29ex  35387  cdlemefr29exN  35415  dibglbN  36180  dihlsscpre  36248  lcfl7N  36515  mapdh9a  36804  mapdh9aOLDN  36805  hdmap11lem2  36859
  Copyright terms: Public domain W3C validator