MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp3d Structured version   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  6845  erinxp  6978  resixp  7097  domssex2  7267  cantnflem1c  7643  cantnflem1  7645  cantnflem3  7647  cantnflem4  7648  fpwwe2lem7  8511  canthnumlem  8523  canthp1lem2  8528  wununi  8581  wunpw  8582  wunpr  8584  ixxdisj  10931  ixxun  10932  ixxss1  10934  ixxss2  10935  ixxss12  10936  ixxub  10937  ixxlb  10938  lbioo  10947  iccsupr  10997  icodisj  11022  xov1plusxeqvd  11041  intfracq  11240  fldiv  11241  seqf1olem2  11363  cjmul  11947  icco1  12334  rpnnen2lem10  12823  ruclem2  12831  ruclem3  12832  ruclem9  12837  ruclem12  12840  dvdslegcd  13016  crt  13167  eulerthlem1  13170  eulerthlem2  13171  pcpremul  13217  prmreclem2  13285  prmreclem3  13286  4sqlem13  13325  sectcan  13981  sectco  13982  sectmon  14003  monsect  14004  funcid  14067  funcco  14068  funcsect  14069  invfuc  14171  fuciso  14172  coapm  14226  catciso  14262  postr  14410  ipodrsima  14591  psref2  14636  psasym  14642  mhm0  14746  submcl  14753  submmnd  14754  eqger  14990  eqgcpbl  14994  gaorber  15085  orbsta  15090  cayleyth  15113  dfod2  15200  sylow2blem1  15254  sylow2blem3  15256  dprdcntz  15566  dprddisj  15567  dprdffi  15572  dpjdisj  15611  ablfac1a  15627  ablfac1b  15628  lmodvsdir  15974  lmhmlin  16111  lbsind  16152  2idlcpbl  16305  assasca  16381  mnfnei  17285  cnprcl  17309  lmcvg  17326  lmff  17365  lmcls  17366  lmcnp  17368  fbasssin  17868  flimfil  18001  tgpconcomp  18142  tlmtrg  18219  ustssel  18235  ustincl  18237  ustdiag  18238  ustinvel  18239  ustexhalf  18240  ustfilxp  18242  tustopn  18301  tususp  18302  imasdsf1olem  18403  xmeter  18463  xmetresbl  18467  tmstopn  18515  metustexhalfOLD  18593  metustexhalf  18594  nlmnrg  18715  qdensere  18804  blcvx  18829  tgqioo  18831  icccmplem1  18853  icccmplem2  18854  reconnlem1  18857  cnmpt2pc  18953  iccpnfcnv  18969  phtpcer  19020  phtpcco2  19024  pcohtpy  19045  pcorev2  19053  pcophtb  19054  om1addcl  19058  pi1blem  19064  pi1cpbl  19069  pi1grplem  19074  pi1inv  19077  pi1xfrf  19078  pi1xfr  19080  pi1xfrcnvlem  19081  pi1cof  19084  pi1coghm  19086  cphreccllem  19141  cphsca  19142  cphsubrg  19143  cphsqrcl2  19149  tchclm  19189  tchcph  19194  lmmcvg  19214  cmetcaulem  19241  lmcau  19265  bcthlem3  19279  bcthlem4  19280  minveclem4c  19326  minveclem2  19327  minveclem3b  19329  minveclem4  19333  minveclem6  19335  ivthicc  19355  ovollb2lem  19384  ovolshftlem1  19405  ovolscalem1  19409  ovolicc1  19412  ovolicc2lem2  19414  ovolicc2lem3  19415  ovolicc2lem4  19416  ovolicc2lem5  19417  ioombl1lem1  19452  dyadmaxlem  19489  volivth  19499  vitalilem2  19501  vitalilem4  19503  i1fima2  19571  itg2monolem1  19642  itgcnlem  19681  itgrevallem1  19686  itgreval  19688  itgle  19701  ibladd  19712  iblabslem  19719  itgspliticc  19728  itgsplitioo  19729  ditgcl  19745  ditgswap  19746  ditgsplitlem  19747  limcdif  19763  limcresi  19772  limcres  19773  limccnp  19778  limccnp2  19779  limcun  19782  dvlip  19877  dvlip2  19879  dveq0  19884  dvgt0lem1  19886  dvivthlem1  19892  dvcnvrelem1  19901  dvcnvre  19903  dvfsumlem2  19911  ftc1lem1  19919  ftc1lem2  19920  ftc1a  19921  ftc1lem4  19923  ftc2  19928  ftc2ditglem  19929  itgsubstlem  19932  mpfind  19965  ply1rem  20086  fta1glem2  20089  ig1pdvds  20099  plyrem  20222  fta1lem  20224  vieta1lem2  20228  aaliou3lem3  20261  pserulm  20338  psercnlem2  20340  psercnlem1  20341  psercn  20342  pserdvlem1  20343  pserdvlem2  20344  abelth2  20358  coseq00topi  20410  coseq0negpitopi  20411  cosordlem  20433  tanord1  20439  efif1olem1  20444  dvloglem  20539  efopnlem1  20547  logreclem  20660  chordthmlem4  20676  quart1  20696  quartlem2  20698  quartlem3  20699  quart  20701  acosbnd  20740  atancj  20750  atanlogsublem  20755  atantan  20763  atanbndlem  20765  atans2  20771  dvatan  20775  atantayl  20777  divsqrsumlem  20818  ftalem5  20859  basellem5  20867  ppisval  20886  chtleppi  20994  chpchtsum  21003  chpub  21004  mersenne  21011  perfectlem2  21014  dchrinv  21045  rplogsumlem2  21179  chpdifbndlem1  21247  pntibndlem2  21285  pntlema  21290  pntlemb  21291  pntlemg  21292  pntlemh  21293  pntlemr  21296  pntlemj  21297  pntlemf  21299  pntlemk  21300  pntlemo  21301  pntlemp  21304  pntleml  21305  abvcxp  21309  ostth2lem2  21328  wlkonwlk  21535  eupapf  21694  tncp  21766  grpolidinv  21789  nvs  22151  nvz  22158  nvtri  22159  sspn  22235  minvecolem2  22377  minvecolem4c  22381  minvecolem4  22382  minvecolem5  22383  minvecolem6  22384  adj1  23436  eliccelico  24140  elicoelioo  24141  cnre2csqlem  24308  rnlogbval  24400  rnlogbcl  24401  nnlogbexp  24404  logbrec  24405  sigaclci  24515  unelsiga  24517  insiga  24520  measvun  24563  cntmeas  24580  sibfima  24653  sibfof  24654  subfacp1lem3  24868  subfacp1lem4  24869  subfacp1lem5  24870  sconpht2  24925  sconpi1  24926  txscon  24928  rescon  24933  cvmcn  24949  cvmsuni  24956  cvmsdisj  24957  cvmshmeo  24958  cvmlift2lem8  24997  cvmlift2lem13  25002  cvmliftphtlem  25004  cvmliftpht  25005  cvmlift3lem6  25011  ghomgrplem  25100  ibladdnc  26262  iblabsnclem  26268  ftc2nc  26289  ivthALT  26338  isbndx  26491  isbnd3  26493  prdsbnd  26502  heiborlem3  26522  iccbnd  26549  rngohomadd  26585  rngohommul  26586  idladdcl  26629  idllmulcl  26630  idlrmulcl  26631  maxidlmax  26653  pridlc  26681  acongrep  27045  pmtrfinv  27379  pmtrfmvdn0  27380  stoweidlem11  27736  stoweidlem31  27756  stoweidlem36  27761  stoweidlem38  27763  stoweidlem62  27787  sigardiv  27827  sigarcol  27830  sharhght  27831  sigaradd  27832  cevathlem1  27833  cevathlem2  27834  cevath  27835  el2wlksoton  28345  el2spthsoton  28346  bnj1018  29333  lshpnelb  29782  lshpcmp  29786  oplecon3  29997  opnoncon  30006  hlcvl  30157  dochshpncl  32182  lclkrslem1  32335  lclkrslem2  32336
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