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  2260  mo2vOLD  2261  mo2vOLDOLD  2262  mopick2  2348  2eu6  2371  cgsexg  3026  cgsex2g  3027  cgsex4g  3028  reximdva0  3669  difsn  4029  preq12b  4069  ordtr2  4784  elres  5166  relssres  5168  elunirn  5989  fnoprabg  6212  tz7.49  6921  omord  7028  ficard  8750  fpwwe2lem12  8829  1idpr  9219  xrsupsslem  11290  xrinfmsslem  11291  fzospliti  11602  sqr2irr  13552  algcvga  13775  prmind2  13795  infpn2  13995  grpinveu  15593  1stcrest  19079  fgss2  19469  fgcl  19473  filufint  19515  metrest  20121  reconnlem2  20426  plydivex  21785  ftalem3  22434  chtub  22573  2sqlem10  22735  dchrisum0flb  22781  pntpbnd1  22857  grpoidinvlem3  23715  grpoinveu  23731  ifbieq12d2  25925  elim2ifim  25929  iocinif  26093  tpr2rico  26364  dfon2lem8  27625  dftrpred3g  27719  nofulllem5  27869  voliunnfl  28461  nn0prpwlem  28543  2pthfrgrarn2  30628  ax6e2eq  31362  bnj168  31817  dalem20  33433  elpaddn0  33540  cdleme25a  34093  cdleme29ex  34114  cdlemefr29exN  34142  dibglbN  34907  dihlsscpre  34975  lcfl7N  35242  mapdh9a  35531  mapdh9aOLDN  35532  hdmap11lem2  35586
  Copyright terms: Public domain W3C validator