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

Theorem simp3d 971
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
31, 2syl 16 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simp3bi  974  oeeui  6804  erinxp  6937  resixp  7056  domssex2  7226  cantnflem1c  7599  cantnflem1  7601  cantnflem3  7603  cantnflem4  7604  fpwwe2lem7  8467  canthnumlem  8479  canthp1lem2  8484  wununi  8537  wunpw  8538  wunpr  8540  ixxdisj  10887  ixxun  10888  ixxss1  10890  ixxss2  10891  ixxss12  10892  ixxub  10893  ixxlb  10894  lbioo  10903  iccsupr  10953  icodisj  10978  xov1plusxeqvd  10997  intfracq  11195  fldiv  11196  seqf1olem2  11318  cjmul  11902  icco1  12289  rpnnen2lem10  12778  ruclem2  12786  ruclem3  12787  ruclem9  12792  ruclem12  12795  dvdslegcd  12971  crt  13122  eulerthlem1  13125  eulerthlem2  13126  pcpremul  13172  prmreclem2  13240  prmreclem3  13241  4sqlem13  13280  sectcan  13936  sectco  13937  sectmon  13958  monsect  13959  funcid  14022  funcco  14023  funcsect  14024  invfuc  14126  fuciso  14127  coapm  14181  catciso  14217  postr  14365  ipodrsima  14546  psref2  14591  psasym  14597  mhm0  14701  submcl  14708  submmnd  14709  eqger  14945  eqgcpbl  14949  gaorber  15040  orbsta  15045  cayleyth  15068  dfod2  15155  sylow2blem1  15209  sylow2blem3  15211  dprdcntz  15521  dprddisj  15522  dprdffi  15527  dpjdisj  15566  ablfac1a  15582  ablfac1b  15583  lmodvsdir  15929  lmhmlin  16066  lbsind  16107  2idlcpbl  16260  assasca  16336  mnfnei  17239  cnprcl  17263  lmcvg  17280  lmff  17319  lmcls  17320  lmcnp  17322  fbasssin  17821  flimfil  17954  tgpconcomp  18095  tlmtrg  18172  ustssel  18188  ustincl  18190  ustdiag  18191  ustinvel  18192  ustexhalf  18193  ustfilxp  18195  tustopn  18254  tususp  18255  imasdsf1olem  18356  xmeter  18416  xmetresbl  18420  tmstopn  18468  metustexhalfOLD  18546  metustexhalf  18547  nlmnrg  18668  qdensere  18757  blcvx  18782  tgqioo  18784  icccmplem1  18806  icccmplem2  18807  reconnlem1  18810  cnmpt2pc  18906  iccpnfcnv  18922  phtpcer  18973  phtpcco2  18977  pcohtpy  18998  pcorev2  19006  pcophtb  19007  om1addcl  19011  pi1blem  19017  pi1cpbl  19022  pi1grplem  19027  pi1inv  19030  pi1xfrf  19031  pi1xfr  19033  pi1xfrcnvlem  19034  pi1cof  19037  pi1coghm  19039  cphreccllem  19094  cphsca  19095  cphsubrg  19096  cphsqrcl2  19102  tchclm  19142  tchcph  19147  lmmcvg  19167  cmetcaulem  19194  lmcau  19218  bcthlem3  19232  bcthlem4  19233  minveclem4c  19279  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  ivthicc  19308  ovollb2lem  19337  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ovolicc2lem2  19367  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  ioombl1lem1  19405  dyadmaxlem  19442  volivth  19452  vitalilem2  19454  vitalilem4  19456  i1fima2  19524  itg2monolem1  19595  itgcnlem  19634  itgrevallem1  19639  itgreval  19641  itgle  19654  ibladd  19665  iblabslem  19672  itgspliticc  19681  itgsplitioo  19682  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  limcdif  19716  limcresi  19725  limcres  19726  limccnp  19731  limccnp2  19732  limcun  19735  dvlip  19830  dvlip2  19832  dveq0  19837  dvgt0lem1  19839  dvivthlem1  19845  dvcnvrelem1  19854  dvcnvre  19856  dvfsumlem2  19864  ftc1lem1  19872  ftc1lem2  19873  ftc1a  19874  ftc1lem4  19876  ftc2  19881  ftc2ditglem  19882  itgsubstlem  19885  mpfind  19918  ply1rem  20039  fta1glem2  20042  ig1pdvds  20052  plyrem  20175  fta1lem  20177  vieta1lem2  20181  aaliou3lem3  20214  pserulm  20291  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  abelth2  20311  coseq00topi  20363  coseq0negpitopi  20364  cosordlem  20386  tanord1  20392  efif1olem1  20397  dvloglem  20492  efopnlem1  20500  logreclem  20613  chordthmlem4  20629  quart1  20649  quartlem2  20651  quartlem3  20652  quart  20654  acosbnd  20693  atancj  20703  atanlogsublem  20708  atantan  20716  atanbndlem  20718  atans2  20724  dvatan  20728  atantayl  20730  divsqrsumlem  20771  ftalem5  20812  basellem5  20820  ppisval  20839  chtleppi  20947  chpchtsum  20956  chpub  20957  mersenne  20964  perfectlem2  20967  dchrinv  20998  rplogsumlem2  21132  chpdifbndlem1  21200  pntibndlem2  21238  pntlema  21243  pntlemb  21244  pntlemg  21245  pntlemh  21246  pntlemr  21249  pntlemj  21250  pntlemf  21252  pntlemk  21253  pntlemo  21254  pntlemp  21257  pntleml  21258  abvcxp  21262  ostth2lem2  21281  wlkonwlk  21488  eupapf  21647  tncp  21719  grpolidinv  21742  nvs  22104  nvz  22111  nvtri  22112  sspn  22188  minvecolem2  22330  minvecolem4c  22334  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  adj1  23389  eliccelico  24093  elicoelioo  24094  cnre2csqlem  24261  rnlogbval  24353  rnlogbcl  24354  nnlogbexp  24357  logbrec  24358  sigaclci  24468  unelsiga  24470  insiga  24473  measvun  24516  cntmeas  24533  sibfima  24606  sibfof  24607  subfacp1lem3  24821  subfacp1lem4  24822  subfacp1lem5  24823  sconpht2  24878  sconpi1  24879  txscon  24881  rescon  24886  cvmcn  24902  cvmsuni  24909  cvmsdisj  24910  cvmshmeo  24911  cvmlift2lem8  24950  cvmlift2lem13  24955  cvmliftphtlem  24957  cvmliftpht  24958  cvmlift3lem6  24964  ghomgrplem  25053  ibladdnc  26161  iblabsnclem  26167  ivthALT  26228  isbndx  26381  isbnd3  26383  prdsbnd  26392  heiborlem3  26412  iccbnd  26439  rngohomadd  26475  rngohommul  26476  idladdcl  26519  idllmulcl  26520  idlrmulcl  26521  maxidlmax  26543  pridlc  26571  acongrep  26935  pmtrfinv  27270  pmtrfmvdn0  27271  stoweidlem11  27627  stoweidlem31  27647  stoweidlem36  27652  stoweidlem38  27654  stoweidlem62  27678  sigardiv  27718  sigarcol  27721  sharhght  27722  sigaradd  27723  cevathlem1  27724  cevathlem2  27725  cevath  27726  el2wlksoton  28075  el2spthsoton  28076  bnj1018  29039  lshpnelb  29467  lshpcmp  29471  oplecon3  29682  opnoncon  29691  hlcvl  29842  dochshpncl  31867  lclkrslem1  32020  lclkrslem2  32021
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator