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  2273  mo2vOLD  2274  mo2vOLDOLD  2275  mopick2  2346  2eu6  2367  cgsexg  3126  cgsex2g  3127  cgsex4g  3128  reximdva0  3778  difsn  4145  preq12b  4187  ordtr2  4908  elres  5295  relssres  5297  elunirn  6144  fnoprabg  6384  tz7.49  7108  omord  7215  ficard  8938  fpwwe2lem12  9017  1idpr  9405  xrsupsslem  11502  xrinfmsslem  11503  fzospliti  11831  sqrt2irr  13854  algcvga  14080  prmind2  14100  infpn2  14303  grpinveu  15953  1stcrest  19820  fgss2  20241  fgcl  20245  filufint  20287  metrest  20893  reconnlem2  21198  plydivex  22558  ftalem3  23213  chtub  23352  2sqlem10  23514  dchrisum0flb  23560  pntpbnd1  23636  2pthfrgrarn2  24875  grpoidinvlem3  25073  grpoinveu  25089  ifbieq12d2  27285  elim2ifim  27288  iocinif  27457  tpr2rico  27760  dfon2lem8  29190  dftrpred3g  29284  nofulllem5  29434  voliunnfl  30026  nn0prpwlem  30108  ax6e2eq  33038  bnj168  33493  dalem20  35119  elpaddn0  35226  cdleme25a  35781  cdleme29ex  35802  cdlemefr29exN  35830  dibglbN  36595  dihlsscpre  36663  lcfl7N  36930  mapdh9a  37219  mapdh9aOLDN  37220  hdmap11lem2  37274
  Copyright terms: Public domain W3C validator