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

Theorem ancld 537
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 22 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 520 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mopick2  2347  cgsexg  2979  cgsex2g  2980  cgsex4g  2981  reximdva0  3631  difsn  3925  preq12b  3966  ordtr2  4617  elres  5173  relssres  5175  elunirnALT  5992  fnoprabg  6163  tz7.49  6694  omord  6803  ficard  8432  fpwwe2lem12  8508  1idpr  8898  xrsupsslem  10877  xrinfmsslem  10878  fzospliti  11157  sqr2irr  12840  algcvga  13062  prmind2  13082  infpn2  13273  grpinveu  14831  1stcrest  17508  fgss2  17898  fgcl  17902  filufint  17944  metrest  18546  reconnlem2  18850  plydivex  20206  ftalem3  20849  chtub  20988  2sqlem10  21150  dchrisum0flb  21196  pntpbnd1  21272  grpoidinvlem3  21786  grpoinveu  21802  ifbieq12d2  23994  elim2ifim  23998  iocinif  24136  tpr2rico  24302  dfon2lem8  25409  dftrpred3g  25503  nofulllem5  25653  voliunnfl  26240  nn0prpwlem  26316  2pthfrgrarn2  28337  a9e2eq  28581  bnj168  29034  dalem20  30427  elpaddn0  30534  cdleme25a  31087  cdleme29ex  31108  cdlemefr29exN  31136  dibglbN  31901  dihlsscpre  31969  lcfl7N  32236  mapdh9a  32525  mapdh9aOLDN  32526  hdmap11lem2  32580
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator