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

Theorem simp3d 1067
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 1055 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simp3bi  1070  f1dom3fv3dif  6403  f1dom3el3dif  6404  oeeui  7546  erinxp  7685  resixp  7806  domssex2  7982  cantnflem1c  8444  cantnflem1  8446  cantnflem3  8448  cantnflem4  8449  fpwwe2lem7  9314  canthnumlem  9326  canthp1lem2  9331  wununi  9384  wunpw  9385  wunpr  9387  lelttrdi  10050  ixxdisj  12017  ixxun  12018  ixxss1  12020  ixxss2  12021  ixxss12  12022  ixxub  12023  ixxlb  12024  lbioo  12033  elicore  12053  iccsupr  12093  icodisj  12124  xov1plusxeqvd  12145  intfracq  12475  fldiv  12476  seqf1olem2  12658  cjmul  13676  icco1  14065  sumtp  14268  rpnnen2lem10  14737  ruclem2  14746  ruclem3  14747  ruclem9  14752  ruclem12  14755  dvdslegcd  15010  crth  15267  eulerthlem1  15270  eulerthlem2  15271  pcpremul  15332  prmreclem2  15405  prmreclem3  15406  4sqlem13  15445  sectcan  16184  sectco  16185  sectmon  16211  monsect  16212  funcid  16299  funcco  16300  funcsect  16301  invfuc  16403  fuciso  16404  coapm  16490  catciso  16526  postr  16722  ipodrsima  16934  psref2  16973  psasym  16979  mhm0  17112  submcl  17122  submmnd  17123  eqger  17413  eqgcpbl  17417  gaorber  17510  orbsta  17515  cayleyth  17604  pmtrrn2  17649  pmtrfinv  17650  pmtrfmvdn0  17651  dfod2  17750  sylow2blem1  17804  sylow2blem3  17806  dprdcntz  18176  dprddisj  18177  dprdffsupp  18182  dpjdisj  18221  ablfac1a  18237  ablfac1b  18238  lmodvsdir  18656  lmhmlin  18802  lbsind  18847  2idlcpbl  19001  assasca  19088  mpfind  19303  mpt2frlmd  19877  mdetunilem2  20180  mdetunilem5  20183  mdetunilem6  20184  mnfnei  20777  cnprcl  20801  lmcvg  20818  lmff  20857  lmcls  20858  lmcnp  20860  fbasssin  21392  flimfil  21525  tgpconcomp  21668  tlmtrg  21745  ustssel  21761  ustincl  21763  ustdiag  21764  ustinvel  21765  ustexhalf  21766  ustfilxp  21768  tustopn  21827  tususp  21828  imasdsf1olem  21929  xmeter  21989  xmetresbl  21993  tmstopn  22041  metustexhalf  22112  nlmnrg  22226  qdensere  22315  blcvx  22341  tgqioo  22343  icccmplem1  22365  icccmplem2  22366  reconnlem1  22369  cnmpt2pc  22466  iccpnfcnv  22482  phtpcer  22533  phtpcerOLD  22534  phtpcco2  22538  pcohtpy  22559  pcorev2  22567  pcophtb  22568  om1addcl  22572  pi1blem  22578  pi1cpbl  22583  pi1grplem  22588  pi1inv  22591  pi1xfrf  22592  pi1xfr  22594  pi1xfrcnvlem  22595  pi1cof  22598  pi1coghm  22600  cphreccllem  22710  cphsca  22711  cphsubrg  22712  cphsqrtcl2  22718  tchclm  22760  tchcph  22765  lmmcvg  22785  cmetcaulem  22812  lmcau  22836  bcthlem3  22848  bcthlem4  22849  minveclem4c  22921  minveclem2  22922  minveclem3b  22924  minveclem4  22928  minveclem6  22930  ivthicc  22951  ovollb2lem  22980  ovolshftlem1  23001  ovolscalem1  23005  ovolicc1  23008  ovolicc2lem2  23010  ovolicc2lem3  23011  ovolicc2lem4  23012  ovolicc2lem5  23013  ioombl1lem1  23050  dyadmaxlem  23088  volivth  23098  vitalilem2  23101  vitalilem4  23103  i1fima2  23169  itg2monolem1  23240  itgcnlem  23279  itgrevallem1  23284  itgreval  23286  itgle  23299  ibladd  23310  iblabslem  23317  itgspliticc  23326  itgsplitioo  23327  ditgcl  23345  ditgswap  23346  ditgsplitlem  23347  limcdif  23363  limcresi  23372  limcres  23373  limccnp  23378  limccnp2  23379  limcun  23382  dvlip  23477  dvlip2  23479  dveq0  23484  dvgt0lem1  23486  dvivthlem1  23492  dvcnvrelem1  23501  dvcnvre  23503  dvfsumlem2  23511  ftc1lem1  23519  ftc1lem2  23520  ftc1a  23521  ftc1lem4  23523  ftc2  23528  ftc2ditglem  23529  itgsubstlem  23532  ply1rem  23644  fta1glem2  23647  ig1pdvds  23657  plyrem  23781  fta1lem  23783  vieta1lem2  23787  aaliou3lem3  23820  pserulm  23897  psercnlem2  23899  psercnlem1  23900  psercn  23901  pserdvlem1  23902  pserdvlem2  23903  abelth2  23917  coseq00topi  23975  coseq0negpitopi  23976  cosordlem  23998  tanord1  24004  efif1olem1  24009  dvloglem  24111  efopnlem1  24119  logreclem  24217  relogbval  24227  nnlogbexp  24236  logbrec  24237  chordthmlem4  24279  quart1  24300  quartlem2  24302  quartlem3  24303  quart  24305  acosbnd  24344  atancj  24354  atanlogsublem  24359  atantan  24367  atanbndlem  24369  atans2  24375  dvatan  24379  atantayl  24381  divsqrtsumlem  24423  ftalem5  24520  basellem5  24528  ppisval  24547  chtleppi  24652  chpchtsum  24661  chpub  24662  mersenne  24669  perfectlem2  24672  dchrinv  24703  rplogsumlem2  24891  chpdifbndlem1  24959  pntibndlem2  24997  pntlema  25002  pntlemb  25003  pntlemg  25004  pntlemh  25005  pntlemr  25008  pntlemj  25009  pntlemf  25011  pntlemk  25012  pntlemo  25013  pntlemp  25016  pntleml  25017  abvcxp  25021  ostth2lem2  25040  axtgcont1  25084  cgr3simp3  25135  legso  25212  hlln  25220  hltr  25223  btwnhl  25227  mirhl  25292  mirbtwnhl  25293  opphllem4  25360  opphl  25364  hlpasch  25366  cgracgr  25428  cgraswap  25430  cgrahl  25436  cgracol  25437  inagswap  25448  wlkonwlk  25831  wwlksswrd  25982  wwlkeq  26016  clwwisshclwwn  26102  erclwwlksym  26108  erclwwlktr  26109  el2wlksoton  26171  el2spthsoton  26172  cusgraiffrusgra  26233  eupapf  26265  frrusgraord  26364  tncp  26487  grpolidinv  26505  nvs  26695  nvz  26702  nvtri  26703  sspn  26779  minvecolem2  26921  minvecolem4c  26925  minvecolem4  26926  minvecolem5  26927  minvecolem6  26928  adj1  27982  eliccelico  28735  elicoelioo  28736  slmdvsdir  28906  slmd0vs  28914  pmtrto1cl  28986  locfinreflem  29041  cnre2csqlem  29090  sigaclci  29328  unelsiga  29330  insiga  29333  unelldsys  29354  ldsysgenld  29356  sigapildsys  29358  ldgenpisyslem1  29359  measvun  29405  cntmeas  29422  sibfima  29533  signstfveq0  29786  tg5segofs  29810  bnj1018  30092  subfacp1lem3  30224  subfacp1lem4  30225  subfacp1lem5  30226  sconpht2  30280  sconpi1  30281  txscon  30283  rescon  30288  cvmcn  30304  cvmsuni  30311  cvmsdisj  30312  cvmshmeo  30313  cvmlift2lem8  30352  cvmlift2lem13  30357  cvmliftphtlem  30359  cvmliftpht  30360  cvmlift3lem6  30366  msrf  30499  elmsta  30505  mthmpps  30539  mclsppslem  30540  ivthALT  31306  relowlssretop  32183  ibladdnc  32433  iblabsnclem  32439  ftc2nc  32460  dvasin  32462  isbndx  32547  isbnd3  32549  prdsbnd  32558  heiborlem3  32578  iccbnd  32605  rngohomadd  32734  rngohommul  32735  idladdcl  32784  idllmulcl  32785  idlrmulcl  32786  maxidlmax  32808  pridlc  32836  lshpnelb  33085  lshpcmp  33089  oplecon3  33300  opnoncon  33309  hlcvl  33460  dochshpncl  35487  lclkrslem1  35640  lclkrslem2  35641  acongrep  36361  ntrneinex  37191  neicvgmex  37231  gneispace0nelrn  37254  cvgdvgrat  37330  binomcxplemdvbinom  37370  fvixp2  38180  eliocre  38378  iccshift  38388  iccsuble  38389  icoiccdif  38394  mullimc  38480  limccog  38484  limciccioolb  38485  mullimcf  38487  limcperiod  38492  lptioo2  38495  lptioo1  38496  neglimc  38511  addlimc  38512  0ellimcdiv  38513  reclimc  38517  icccncfext  38570  cncfioobdlem  38579  ditgeqiooicc  38649  iblspltprt  38662  iblcncfioo  38667  itgiccshift  38669  itgperiod  38670  itgsbtaddcnst  38671  stoweidlem11  38701  stoweidlem31  38721  stoweidlem36  38726  stoweidlem38  38728  stoweidlem62  38752  dirkercncflem1  38793  dirkercncflem4  38796  fourierdlem26  38823  fourierdlem32  38829  fourierdlem33  38830  fourierdlem37  38834  fourierdlem42  38839  fourierdlem54  38850  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem74  38870  fourierdlem75  38871  fourierdlem79  38875  fourierdlem81  38877  fourierdlem82  38878  fourierdlem89  38885  fourierdlem90  38886  fourierdlem91  38887  fourierdlem93  38889  fourierdlem101  38897  fourierdlem107  38903  fourierdlem109  38905  fourierdlem111  38907  salunicl  39009  saluncl  39010  hoidmv1lelem1  39278  hoidmv1lelem3  39280  hoidmvlelem1  39282  ovolval3  39334  iinhoiicclem  39361  smfpreimalt  39414  smfpreimaltf  39420  smfpreimale  39438  issmfgt  39440  smfpreimagt  39445  smfpreimage  39465  sigardiv  39496  sigarcol  39499  sharhght  39500  sigaradd  39501  cevathlem1  39502  cevathlem2  39503  cevath  39504  proththd  39867  perfectALTVlem2  39963  umgrnloopv  40326  umgredgne  40370  usgrnloopvALT  40423  frusgrnn0  40766  cusgrm1rusgr  40777  upgrclwlkcompim  40983  21wlkdlem6  41133  21wlkond  41139  2trlond  41141  av-numclwwlk2lem1  41527
  Copyright terms: Public domain W3C validator