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

Theorem simp3d 1144
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.)
Hypothesis
Ref Expression
3simp1d.1 (𝜑 → (𝜓𝜒𝜃))
Assertion
Ref Expression
simp3d (𝜑𝜃)

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp3 1138 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7211  f1dom3el3dif  7212  oeeui  8545  resixp  8867  domssex2  9077  cantnflem1c  9619  cantnflem1  9621  cantnflem3  9623  cantnflem4  9624  fpwwe2lem6  10568  canthnumlem  10580  canthp1lem2  10585  wununi  10638  wunpw  10639  wunpr  10641  lelttrdi  11313  ixxdisj  13271  ixxun  13272  ixxss1  13274  ixxss2  13275  ixxss12  13276  ixxub  13277  ixxlb  13278  lbioo  13287  elicore  13308  iccsupr  13351  icodisj  13385  xov1plusxeqvd  13407  intfracq  13756  fldiv  13757  seqf1olem2  13940  cjmul  15019  icco1  15414  sumtp  15626  rpnnen2lem10  16097  ruclem2  16106  ruclem3  16107  ruclem9  16112  ruclem12  16115  dvdslegcd  16376  crth  16642  eulerthlem1  16645  eulerthlem2  16646  pcpremul  16707  prmreclem2  16781  prmreclem3  16782  4sqlem13  16821  sectcan  17630  sectco  17631  sectmon  17657  monsect  17658  funcid  17748  funcco  17749  funcsect  17750  invfuc  17855  fuciso  17856  coapm  17949  catciso  17989  postr  18201  ipodrsima  18422  psref2  18451  psasym  18457  mhm0  18602  submcl  18615  submmnd  18616  eqger  18971  eqgcpbl  18975  gaorber  19079  orbsta  19084  cayleyth  19188  pmtrrn2  19233  pmtrfinv  19234  pmtrfmvdn0  19235  dfod2  19337  sylow2blem1  19393  sylow2blem3  19395  dprdcntz  19778  dprddisj  19779  dprdffsupp  19784  dpjdisj  19823  ablfac1a  19839  ablfac1b  19840  lmodvsdir  20331  lmhmlin  20481  lbsind  20526  2idlcpbl  20689  assasca  21253  mpfind  21501  mdetunilem2  21946  mdetunilem5  21949  mdetunilem6  21950  mnfnei  22556  cnprcl  22580  lmcvg  22597  lmff  22636  lmcls  22637  lmcnp  22639  fbasssin  23171  flimfil  23304  tgpconncomp  23448  tlmtrg  23525  ustssel  23541  ustincl  23543  ustdiag  23544  ustinvel  23545  ustexhalf  23546  ustfilxp  23548  tustopn  23607  tususp  23608  imasdsf1olem  23710  xmeter  23770  xmetresbl  23774  tmstopn  23825  metustexhalf  23896  nlmnrg  24027  qdensere  24117  blcvx  24145  tgqioo  24147  icccmplem1  24169  icccmplem2  24170  reconnlem1  24173  cnmpopc  24275  iccpnfcnv  24291  phtpcer  24342  phtpcco2  24346  pcohtpy  24367  pcorev2  24375  pcophtb  24376  om1addcl  24380  pi1blem  24386  pi1cpbl  24391  pi1grplem  24396  pi1inv  24399  pi1xfrf  24400  pi1xfr  24402  pi1xfrcnvlem  24403  pi1cof  24406  pi1coghm  24408  cphreccllem  24526  cphsca  24527  cphsubrg  24528  cphsqrtcl2  24534  phclm  24580  tcphcph  24585  lmmcvg  24609  cmetcaulem  24636  lmcau  24661  bcthlem3  24674  bcthlem4  24675  minveclem4c  24773  minveclem2  24774  minveclem3b  24776  minveclem4  24780  minveclem6  24782  ivthicc  24806  ovollb2lem  24836  ovolshftlem1  24857  ovolscalem1  24861  ovolicc1  24864  ovolicc2lem2  24866  ovolicc2lem3  24867  ovolicc2lem4  24868  ovolicc2lem5  24869  ioombl1lem1  24906  dyadmaxlem  24945  volivth  24955  vitalilem2  24957  vitalilem4  24959  i1fima2  25027  itg2monolem1  25099  itgcnlem  25138  itgrevallem1  25143  itgreval  25145  itgle  25158  ibladd  25169  iblabslem  25176  itgspliticc  25185  itgsplitioo  25186  ditgcl  25206  ditgswap  25207  ditgsplitlem  25208  limcdif  25224  limcresi  25233  limcres  25234  limccnp  25239  limccnp2  25240  limcun  25243  dvlip  25341  dvlip2  25343  dveq0  25348  dvgt0lem1  25350  dvivthlem1  25356  dvcnvrelem1  25365  dvcnvre  25367  dvfsumlem2  25375  ftc1lem1  25383  ftc1lem2  25384  ftc1a  25385  ftc1lem4  25387  ftc2  25392  ftc2ditglem  25393  itgsubstlem  25396  ply1rem  25512  fta1glem2  25515  ig1pdvds  25525  plyrem  25649  fta1lem  25651  vieta1lem2  25655  aaliou3lem3  25688  pserulm  25765  psercnlem2  25767  psercnlem1  25768  psercn  25769  pserdvlem1  25770  pserdvlem2  25771  abelth2  25785  coseq00topi  25843  coseq0negpitopi  25844  cosordlem  25870  tanord1  25877  efif1olem1  25882  dvloglem  25987  efopnlem1  25995  logreclem  26096  relogbval  26106  nnlogbexp  26115  logbrec  26116  chordthmlem4  26169  quart1  26190  quartlem2  26192  quartlem3  26193  quart  26195  acosbnd  26234  atancj  26244  atanlogsublem  26249  atantan  26257  atanbndlem  26259  atans2  26265  dvatan  26269  atantayl  26271  divsqrtsumlem  26313  ftalem5  26410  basellem5  26418  ppisval  26437  chtleppi  26542  chpchtsum  26551  chpub  26552  mersenne  26559  perfectlem2  26562  dchrinv  26593  rplogsumlem2  26817  chpdifbndlem1  26885  pntibndlem2  26923  pntlema  26928  pntlemb  26929  pntlemg  26930  pntlemh  26931  pntlemr  26934  pntlemj  26935  pntlemf  26937  pntlemk  26938  pntlemo  26939  pntlemp  26942  pntleml  26943  abvcxp  26947  ostth2lem2  26966  scutun12  27133  slerec  27142  cofcut2  27225  cofcutr  27227  cofcutrtime  27230  axtgcont1  27296  cgr3simp3  27350  legso  27427  hlln  27435  hltr  27438  btwnhl  27442  mirhl  27507  mirbtwnhl  27508  opphllem4  27578  opphl  27582  hlpasch  27584  cgracgr  27646  cgraswap  27648  cgrahl  27655  cgracol  27656  inagswap  27669  inagne3  27672  dfcgrg2  27691  umgrnloopv  27943  umgredgne  27982  usgrnloopvALT  28035  frusgrnn0  28405  cusgrm1rusgr  28416  upgrclwlkcompim  28615  2wlkdlem6  28762  2wlkond  28768  2trlond  28770  numclwwlk2lem1  29206  numclwlk2lem2f1o  29209  tncp  29306  grpolidinv  29329  nvs  29491  nvz  29497  nvtri  29498  sspn  29564  minvecolem2  29703  minvecolem4c  29707  minvecolem4  29708  minvecolem5  29709  minvecolem6  29710  adj1  30761  eliccelico  31563  elicoelioo  31564  prmdvdsbc  31595  pmtrto1cl  31831  cyc3evpm  31882  slmdvsdir  31934  slmd0vs  31942  sdrgdvcl  31959  sdrginvcl  31960  nsgqusf1olem3  32076  prmidl  32091  prmidlc  32100  qsidomlem2  32105  mxidlmax  32113  0ringmon1p  32143  irngss  32238  locfinreflem  32290  cnre2csqlem  32360  sigaclci  32600  unelsiga  32602  insiga  32605  unelldsys  32626  ldsysgenld  32628  sigapildsys  32630  ldgenpisyslem1  32631  measvun  32677  cntmeas  32694  sibfima  32807  signstfveq0  33058  tg5segofs  33155  bnj1018g  33444  bnj1018  33445  pfxwlk  33586  revwlk  33587  spthcycl  33592  acycgrcycl  33610  subfacp1lem3  33645  subfacp1lem4  33646  subfacp1lem5  33647  sconnpht2  33701  sconnpi1  33702  txsconn  33704  resconn  33709  cvmcn  33725  cvmsuni  33732  cvmsdisj  33733  cvmshmeo  33734  cvmlift2lem8  33773  cvmlift2lem13  33778  cvmliftphtlem  33780  cvmliftpht  33781  cvmlift3lem6  33787  msrf  34005  elmsta  34011  mthmpps  34045  mclsppslem  34046  addsproplem5  34289  addsproplem6  34290  sleadd1  34302  addsunif  34314  addsasslem1  34315  addsasslem2  34316  negsproplem4  34333  negsproplem6  34335  negscut2  34342  ivthALT  34774  relowlssretop  35801  ibladdnc  36102  iblabsnclem  36108  ftc2nc  36127  dvasin  36129  isbndx  36208  isbnd3  36210  prdsbnd  36219  heiborlem3  36239  iccbnd  36266  rngohomadd  36395  rngohommul  36396  idladdcl  36445  idllmulcl  36446  idlrmulcl  36447  maxidlmax  36469  pridlc  36497  eqvreltr  37036  lshpnelb  37413  lshpcmp  37417  oplecon3  37628  opnoncon  37637  hlcvl  37788  dochshpncl  39814  lclkrslem1  39967  lclkrslem2  39968  fzne2d  40405  sticksstones3  40523  metakunt8  40551  metakunt20  40563  metakunt21  40564  metakunt22  40565  metakunt24  40567  metakunt25  40568  evlsval3  40696  flt4lem5f  40933  flt4lem7  40935  nna4b4nsq  40936  acongrep  41242  ntrneinex  42291  neicvgmex  42331  gneispace0nelrn  42354  cvgdvgrat  42535  binomcxplemdvbinom  42575  eliocre  43679  iccshift  43688  iccsuble  43689  icoiccdif  43694  mullimc  43789  limccog  43793  limciccioolb  43794  mullimcf  43796  limcperiod  43801  lptioo2  43804  lptioo1  43805  neglimc  43820  addlimc  43821  0ellimcdiv  43822  reclimc  43826  xlimmnfvlem1  44005  xlimpnfvlem1  44009  icccncfext  44060  cncfioobdlem  44069  ditgeqiooicc  44133  iblspltprt  44146  iblcncfioo  44151  itgiccshift  44153  itgperiod  44154  itgsbtaddcnst  44155  stoweidlem11  44184  stoweidlem31  44204  stoweidlem36  44209  stoweidlem38  44211  stoweidlem62  44235  dirkercncflem1  44276  dirkercncflem4  44279  fourierdlem26  44306  fourierdlem32  44312  fourierdlem33  44313  fourierdlem37  44317  fourierdlem42  44322  fourierdlem54  44333  fourierdlem63  44342  fourierdlem64  44343  fourierdlem65  44344  fourierdlem74  44353  fourierdlem75  44354  fourierdlem79  44358  fourierdlem81  44360  fourierdlem82  44361  fourierdlem89  44368  fourierdlem90  44369  fourierdlem91  44370  fourierdlem93  44372  fourierdlem101  44380  fourierdlem107  44386  fourierdlem109  44388  fourierdlem111  44390  salunicl  44489  saluncl  44490  hoidmv1lelem1  44764  hoidmv1lelem3  44766  hoidmvlelem1  44768  ovolval3  44820  iinhoiicclem  44846  smfpreimalt  44904  smfpreimaltf  44909  smfpreimale  44927  issmfgt  44929  smfpreimagt  44935  smfpreimage  44955  sigardiv  45034  sigarcol  45037  sharhght  45038  sigaradd  45039  cevathlem1  45040  cevathlem2  45041  cevath  45042  proththd  45738  perfectALTVlem2  45846
  Copyright terms: Public domain W3C validator