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

Theorem simp3d 1002
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Assertion
Ref Expression
simp3d  |-  ( ph  ->  th )

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
2 simp3 990 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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  df-3an 967
This theorem is referenced by:  simp3bi  1005  f1dom3fv3dif  5985  f1dom3el3dif  5986  oeeui  7046  erinxp  7179  resixp  7303  domssex2  7476  cantnflem1c  7900  cantnflem1  7902  cantnflem3  7904  cantnflem4  7905  cantnflem1cOLD  7923  cantnflem1OLD  7925  cantnflem3OLD  7926  cantnflem4OLD  7927  fpwwe2lem7  8808  canthnumlem  8820  canthp1lem2  8825  wununi  8878  wunpw  8879  wunpr  8881  ixxdisj  11320  ixxun  11321  ixxss1  11323  ixxss2  11324  ixxss12  11325  ixxub  11326  ixxlb  11327  lbioo  11336  iccsupr  11387  icodisj  11415  xov1plusxeqvd  11436  supicc  11438  intfracq  11703  fldiv  11704  seqf1olem2  11851  cjmul  12636  icco1  13023  rpnnen2lem10  13511  ruclem2  13519  ruclem3  13520  ruclem9  13525  ruclem12  13528  dvdslegcd  13705  crt  13858  eulerthlem1  13861  eulerthlem2  13862  pcpremul  13915  prmreclem2  13983  prmreclem3  13984  4sqlem13  14023  sectcan  14699  sectco  14700  sectmon  14721  monsect  14722  funcid  14785  funcco  14786  funcsect  14787  invfuc  14889  fuciso  14890  coapm  14944  catciso  14980  postr  15128  ipodrsima  15340  psref2  15379  psasym  15385  mhm0  15477  submcl  15486  submmnd  15487  eqger  15736  eqgcpbl  15740  gaorber  15831  orbsta  15836  cayleyth  15925  pmtrrn2  15971  pmtrfinv  15972  pmtrfmvdn0  15973  dfod2  16070  sylow2blem1  16124  sylow2blem3  16126  dprdcntz  16497  dprddisj  16498  dprdffsupp  16503  dprdffiOLD  16509  dpjdisj  16557  ablfac1a  16575  ablfac1b  16576  rngsrg  16688  lmodvsdir  16977  lmhmlin  17121  lbsind  17166  2idlcpbl  17321  assasca  17398  mpfind  17627  mpt2frlmd  18207  mdetunilem2  18424  mdetunilem5  18427  mdetunilem6  18428  mnfnei  18830  cnprcl  18854  lmcvg  18871  lmff  18910  lmcls  18911  lmcnp  18913  fbasssin  19414  flimfil  19547  tgpconcomp  19688  tlmtrg  19769  ustssel  19785  ustincl  19787  ustdiag  19788  ustinvel  19789  ustexhalf  19790  ustfilxp  19792  tustopn  19851  tususp  19852  imasdsf1olem  19953  xmeter  20013  xmetresbl  20017  tmstopn  20065  metustexhalfOLD  20143  metustexhalf  20144  nlmnrg  20265  qdensere  20354  blcvx  20380  tgqioo  20382  icccmplem1  20404  icccmplem2  20405  reconnlem1  20408  cnmpt2pc  20505  iccpnfcnv  20521  phtpcer  20572  phtpcco2  20576  pcohtpy  20597  pcorev2  20605  pcophtb  20606  om1addcl  20610  pi1blem  20616  pi1cpbl  20621  pi1grplem  20626  pi1inv  20629  pi1xfrf  20630  pi1xfr  20632  pi1xfrcnvlem  20633  pi1cof  20636  pi1coghm  20638  cphreccllem  20702  cphsca  20703  cphsubrg  20704  cphsqrcl2  20710  tchclm  20752  tchcph  20757  lmmcvg  20777  cmetcaulem  20804  lmcau  20828  bcthlem3  20842  bcthlem4  20843  minveclem4c  20917  minveclem2  20918  minveclem3b  20920  minveclem4  20924  minveclem6  20926  ivthicc  20947  ovollb2lem  20976  ovolshftlem1  20997  ovolscalem1  21001  ovolicc1  21004  ovolicc2lem2  21006  ovolicc2lem3  21007  ovolicc2lem4  21008  ovolicc2lem5  21009  ioombl1lem1  21044  dyadmaxlem  21082  volivth  21092  vitalilem2  21094  vitalilem4  21096  i1fima2  21162  itg2monolem1  21233  itgcnlem  21272  itgrevallem1  21277  itgreval  21279  itgle  21292  ibladd  21303  iblabslem  21310  itgspliticc  21319  itgsplitioo  21320  ditgcl  21338  ditgswap  21339  ditgsplitlem  21340  limcdif  21356  limcresi  21365  limcres  21366  limccnp  21371  limccnp2  21372  limcun  21375  dvlip  21470  dvlip2  21472  dveq0  21477  dvgt0lem1  21479  dvivthlem1  21485  dvcnvrelem1  21494  dvcnvre  21496  dvfsumlem2  21504  ftc1lem1  21512  ftc1lem2  21513  ftc1a  21514  ftc1lem4  21516  ftc2  21521  ftc2ditglem  21522  itgsubstlem  21525  ply1rem  21640  fta1glem2  21643  ig1pdvds  21653  plyrem  21776  fta1lem  21778  vieta1lem2  21782  aaliou3lem3  21815  pserulm  21892  psercnlem2  21894  psercnlem1  21895  psercn  21896  pserdvlem1  21897  pserdvlem2  21898  abelth2  21912  coseq00topi  21969  coseq0negpitopi  21970  cosordlem  21992  tanord1  21998  efif1olem1  22003  dvloglem  22098  efopnlem1  22106  logreclem  22219  chordthmlem4  22235  quart1  22256  quartlem2  22258  quartlem3  22259  quart  22261  acosbnd  22300  atancj  22310  atanlogsublem  22315  atantan  22323  atanbndlem  22325  atans2  22331  dvatan  22335  atantayl  22337  divsqrsumlem  22378  ftalem5  22419  basellem5  22427  ppisval  22446  chtleppi  22554  chpchtsum  22563  chpub  22564  mersenne  22571  perfectlem2  22574  dchrinv  22605  rplogsumlem2  22739  chpdifbndlem1  22807  pntibndlem2  22845  pntlema  22850  pntlemb  22851  pntlemg  22852  pntlemh  22853  pntlemr  22856  pntlemj  22857  pntlemf  22859  pntlemk  22860  pntlemo  22861  pntlemp  22864  pntleml  22865  abvcxp  22869  ostth2lem2  22888  axtgcont1  22934  cgr3simp3  22979  colline  23057  wlkonwlk  23439  eupapf  23598  tncp  23670  grpolidinv  23693  nvs  24055  nvz  24062  nvtri  24063  sspn  24139  minvecolem2  24281  minvecolem4c  24285  minvecolem4  24286  minvecolem5  24287  minvecolem6  24288  adj1  25342  eliccelico  26072  elicoelioo  26073  slmdvsdir  26237  slmd0vs  26245  cnre2csqlem  26345  rnlogbval  26464  rnlogbcl  26465  nnlogbexp  26468  logbrec  26469  sigaclci  26580  unelsiga  26582  insiga  26585  measvun  26628  cntmeas  26645  sibfima  26729  signstfveq0  26983  tg5segofs  27002  subfacp1lem3  27075  subfacp1lem4  27076  subfacp1lem5  27077  sconpht2  27132  sconpi1  27133  txscon  27135  rescon  27140  cvmcn  27156  cvmsuni  27163  cvmsdisj  27164  cvmshmeo  27165  cvmlift2lem8  27204  cvmlift2lem13  27209  cvmliftphtlem  27211  cvmliftpht  27212  cvmlift3lem6  27218  ghomgrplem  27313  ibladdnc  28454  iblabsnclem  28460  ftc2nc  28481  dvasin  28485  ivthALT  28535  isbndx  28686  isbnd3  28688  prdsbnd  28697  heiborlem3  28717  iccbnd  28744  rngohomadd  28780  rngohommul  28781  idladdcl  28824  idllmulcl  28825  idlrmulcl  28826  maxidlmax  28848  pridlc  28876  acongrep  29328  stoweidlem11  29811  stoweidlem31  29831  stoweidlem36  29836  stoweidlem38  29838  stoweidlem62  29862  sigardiv  29902  sigarcol  29905  sharhght  29906  sigaradd  29907  cevathlem1  29908  cevathlem2  29909  cevath  29910  lelttrdi  30183  wwlksswrd  30327  wwlkeq  30359  el2wlksoton  30402  el2spthsoton  30403  clwwisshclwwn  30477  erclwwlksym  30489  erclwwlktr  30490  cusgraiffrusgra  30558  frrusgraord  30669  bnj1018  31960  lshpnelb  32634  lshpcmp  32638  oplecon3  32849  opnoncon  32858  hlcvl  33009  dochshpncl  35034  lclkrslem1  35187  lclkrslem2  35188
  Copyright terms: Public domain W3C validator