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

Theorem simp3d 995
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 983 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  simp3bi  998  f1dom3fv3dif  5967  f1dom3el3dif  5968  oeeui  7029  erinxp  7162  resixp  7286  domssex2  7459  cantnflem1c  7883  cantnflem1  7885  cantnflem3  7887  cantnflem4  7888  cantnflem1cOLD  7906  cantnflem1OLD  7908  cantnflem3OLD  7909  cantnflem4OLD  7910  fpwwe2lem7  8790  canthnumlem  8802  canthp1lem2  8807  wununi  8860  wunpw  8861  wunpr  8863  ixxdisj  11302  ixxun  11303  ixxss1  11305  ixxss2  11306  ixxss12  11307  ixxub  11308  ixxlb  11309  lbioo  11318  iccsupr  11369  icodisj  11396  xov1plusxeqvd  11417  supicc  11419  intfracq  11681  fldiv  11682  seqf1olem2  11829  cjmul  12614  icco1  13001  rpnnen2lem10  13488  ruclem2  13496  ruclem3  13497  ruclem9  13502  ruclem12  13505  dvdslegcd  13682  crt  13835  eulerthlem1  13838  eulerthlem2  13839  pcpremul  13892  prmreclem2  13960  prmreclem3  13961  4sqlem13  14000  sectcan  14676  sectco  14677  sectmon  14698  monsect  14699  funcid  14762  funcco  14763  funcsect  14764  invfuc  14866  fuciso  14867  coapm  14921  catciso  14957  postr  15105  ipodrsima  15317  psref2  15356  psasym  15362  mhm0  15454  submcl  15462  submmnd  15463  eqger  15710  eqgcpbl  15714  gaorber  15805  orbsta  15810  cayleyth  15899  pmtrrn2  15945  pmtrfinv  15946  pmtrfmvdn0  15947  dfod2  16044  sylow2blem1  16098  sylow2blem3  16100  dprdcntz  16465  dprddisj  16466  dprdffsupp  16471  dprdffiOLD  16477  dpjdisj  16525  ablfac1a  16543  ablfac1b  16544  lmodvsdir  16895  lmhmlin  17037  lbsind  17082  2idlcpbl  17237  assasca  17314  mpt2frlmd  18043  mdetunilem2  18260  mdetunilem5  18263  mdetunilem6  18264  mnfnei  18666  cnprcl  18690  lmcvg  18707  lmff  18746  lmcls  18747  lmcnp  18749  fbasssin  19250  flimfil  19383  tgpconcomp  19524  tlmtrg  19605  ustssel  19621  ustincl  19623  ustdiag  19624  ustinvel  19625  ustexhalf  19626  ustfilxp  19628  tustopn  19687  tususp  19688  imasdsf1olem  19789  xmeter  19849  xmetresbl  19853  tmstopn  19901  metustexhalfOLD  19979  metustexhalf  19980  nlmnrg  20101  qdensere  20190  blcvx  20216  tgqioo  20218  icccmplem1  20240  icccmplem2  20241  reconnlem1  20244  cnmpt2pc  20341  iccpnfcnv  20357  phtpcer  20408  phtpcco2  20412  pcohtpy  20433  pcorev2  20441  pcophtb  20442  om1addcl  20446  pi1blem  20452  pi1cpbl  20457  pi1grplem  20462  pi1inv  20465  pi1xfrf  20466  pi1xfr  20468  pi1xfrcnvlem  20469  pi1cof  20472  pi1coghm  20474  cphreccllem  20538  cphsca  20539  cphsubrg  20540  cphsqrcl2  20546  tchclm  20588  tchcph  20593  lmmcvg  20613  cmetcaulem  20640  lmcau  20664  bcthlem3  20678  bcthlem4  20679  minveclem4c  20753  minveclem2  20754  minveclem3b  20756  minveclem4  20760  minveclem6  20762  ivthicc  20783  ovollb2lem  20812  ovolshftlem1  20833  ovolscalem1  20837  ovolicc1  20840  ovolicc2lem2  20842  ovolicc2lem3  20843  ovolicc2lem4  20844  ovolicc2lem5  20845  ioombl1lem1  20880  dyadmaxlem  20918  volivth  20928  vitalilem2  20930  vitalilem4  20932  i1fima2  20998  itg2monolem1  21069  itgcnlem  21108  itgrevallem1  21113  itgreval  21115  itgle  21128  ibladd  21139  iblabslem  21146  itgspliticc  21155  itgsplitioo  21156  ditgcl  21174  ditgswap  21175  ditgsplitlem  21176  limcdif  21192  limcresi  21201  limcres  21202  limccnp  21207  limccnp2  21208  limcun  21211  dvlip  21306  dvlip2  21308  dveq0  21313  dvgt0lem1  21315  dvivthlem1  21321  dvcnvrelem1  21330  dvcnvre  21332  dvfsumlem2  21340  ftc1lem1  21348  ftc1lem2  21349  ftc1a  21350  ftc1lem4  21352  ftc2  21357  ftc2ditglem  21358  itgsubstlem  21361  mpfind  21395  ply1rem  21519  fta1glem2  21522  ig1pdvds  21532  plyrem  21655  fta1lem  21657  vieta1lem2  21661  aaliou3lem3  21694  pserulm  21771  psercnlem2  21773  psercnlem1  21774  psercn  21775  pserdvlem1  21776  pserdvlem2  21777  abelth2  21791  coseq00topi  21848  coseq0negpitopi  21849  cosordlem  21871  tanord1  21877  efif1olem1  21882  dvloglem  21977  efopnlem1  21985  logreclem  22098  chordthmlem4  22114  quart1  22135  quartlem2  22137  quartlem3  22138  quart  22140  acosbnd  22179  atancj  22189  atanlogsublem  22194  atantan  22202  atanbndlem  22204  atans2  22210  dvatan  22214  atantayl  22216  divsqrsumlem  22257  ftalem5  22298  basellem5  22306  ppisval  22325  chtleppi  22433  chpchtsum  22442  chpub  22443  mersenne  22450  perfectlem2  22453  dchrinv  22484  rplogsumlem2  22618  chpdifbndlem1  22686  pntibndlem2  22724  pntlema  22729  pntlemb  22730  pntlemg  22731  pntlemh  22732  pntlemr  22735  pntlemj  22736  pntlemf  22738  pntlemk  22739  pntlemo  22740  pntlemp  22743  pntleml  22744  abvcxp  22748  ostth2lem2  22767  axtgcont1  22813  cgr3simp3  22854  colline  22917  wlkonwlk  23256  eupapf  23415  tncp  23487  grpolidinv  23510  nvs  23872  nvz  23879  nvtri  23880  sspn  23956  minvecolem2  24098  minvecolem4c  24102  minvecolem4  24103  minvecolem5  24104  minvecolem6  24105  adj1  25159  eliccelico  25889  elicoelioo  25890  rngsrg  26042  slmdvsdir  26080  slmd0vs  26088  cnre2csqlem  26193  rnlogbval  26312  rnlogbcl  26313  nnlogbexp  26316  logbrec  26317  sigaclci  26428  unelsiga  26430  insiga  26433  measvun  26476  cntmeas  26493  sibfima  26571  signstfveq0  26825  tg5segofs  26844  subfacp1lem3  26917  subfacp1lem4  26918  subfacp1lem5  26919  sconpht2  26974  sconpi1  26975  txscon  26977  rescon  26982  cvmcn  26998  cvmsuni  27005  cvmsdisj  27006  cvmshmeo  27007  cvmlift2lem8  27046  cvmlift2lem13  27051  cvmliftphtlem  27053  cvmliftpht  27054  cvmlift3lem6  27060  ghomgrplem  27154  ibladdnc  28290  iblabsnclem  28296  ftc2nc  28317  dvasin  28321  ivthALT  28371  isbndx  28522  isbnd3  28524  prdsbnd  28533  heiborlem3  28553  iccbnd  28580  rngohomadd  28616  rngohommul  28617  idladdcl  28660  idllmulcl  28661  idlrmulcl  28662  maxidlmax  28684  pridlc  28712  acongrep  29165  stoweidlem11  29649  stoweidlem31  29669  stoweidlem36  29674  stoweidlem38  29676  stoweidlem62  29700  sigardiv  29740  sigarcol  29743  sharhght  29744  sigaradd  29745  cevathlem1  29746  cevathlem2  29747  cevath  29748  lelttrdi  30021  wwlksswrd  30165  wwlkeq  30197  el2wlksoton  30240  el2spthsoton  30241  clwwisshclwwn  30315  erclwwlksym  30327  erclwwlktr  30328  cusgraiffrusgra  30396  frrusgraord  30507  bnj1018  31654  lshpnelb  32199  lshpcmp  32203  oplecon3  32414  opnoncon  32423  hlcvl  32574  dochshpncl  34599  lclkrslem1  34752  lclkrslem2  34753
  Copyright terms: Public domain W3C validator