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

Theorem ancld 536
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 21 . 2  |-  ( ph  ->  ( ps  ->  ps ) )
2 ancld.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2jcad 519 1  |-  ( ph  ->  ( ps  ->  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mopick2  2210  cgsexg  2819  cgsex2g  2820  cgsex4g  2821  reximdva0  3466  difsn  3755  preq12b  3788  ordtr2  4436  elres  4990  relssres  4992  elunirnALT  5779  fnoprabg  5945  tz7.49  6457  omord  6566  ficard  8187  fpwwe2lem12  8263  1idpr  8653  xrsupsslem  10625  xrinfmsslem  10626  fzospliti  10898  sqr2irr  12527  algcvga  12749  prmind2  12769  infpn2  12960  grpinveu  14516  1stcrest  17179  fgss2  17569  fgcl  17573  filufint  17615  metrest  18070  reconnlem2  18332  plydivex  19677  ftalem3  20312  chtub  20451  2sqlem10  20613  dchrisum0flb  20659  pntpbnd1  20735  grpoidinvlem3  20873  grpoinveu  20889  ifbieq12d2  23149  elim2ifim  23153  iocinif  23274  tpr2rico  23296  dfon2lem8  24146  dftrpred3g  24236  nofulllem5  24360  prl2  25169  nn0prpwlem  26238  a9e2eq  28323  bnj168  28758  dalem20  29882  elpaddn0  29989  cdleme25a  30542  cdleme29ex  30563  cdlemefr29exN  30591  dibglbN  31356  dihlsscpre  31424  lcfl7N  31691  mapdh9a  31980  mapdh9aOLDN  31981  hdmap11lem2  32035
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 177  df-an 360
  Copyright terms: Public domain W3C validator