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  2223  cgsexg  2832  cgsex2g  2833  cgsex4g  2834  reximdva0  3479  difsn  3768  preq12b  3804  ordtr2  4452  elres  5006  relssres  5008  elunirnALT  5795  fnoprabg  5961  tz7.49  6473  omord  6582  ficard  8203  fpwwe2lem12  8279  1idpr  8669  xrsupsslem  10641  xrinfmsslem  10642  fzospliti  10914  sqr2irr  12543  algcvga  12765  prmind2  12785  infpn2  12976  grpinveu  14532  1stcrest  17195  fgss2  17585  fgcl  17589  filufint  17631  metrest  18086  reconnlem2  18348  plydivex  19693  ftalem3  20328  chtub  20467  2sqlem10  20629  dchrisum0flb  20675  pntpbnd1  20751  grpoidinvlem3  20889  grpoinveu  20905  ifbieq12d2  23165  elim2ifim  23169  iocinif  23289  tpr2rico  23311  dfon2lem8  24217  dftrpred3g  24307  nofulllem5  24431  prl2  25272  nn0prpwlem  26341  2pthfrgrarn2  28434  a9e2eq  28622  bnj168  29074  dalem20  30504  elpaddn0  30611  cdleme25a  31164  cdleme29ex  31185  cdlemefr29exN  31213  dibglbN  31978  dihlsscpre  32046  lcfl7N  32313  mapdh9a  32602  mapdh9aOLDN  32603  hdmap11lem2  32657
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