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

Theorem simp3d 1136
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 1130 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  simp3bi  1139  f1dom3fv3dif  7017  f1dom3el3dif  7018  oeeui  8218  resixp  8486  domssex2  8666  cantnflem1c  9139  cantnflem1  9141  cantnflem3  9143  cantnflem4  9144  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wununi  10117  wunpw  10118  wunpr  10120  lelttrdi  10791  ixxdisj  12743  ixxun  12744  ixxss1  12746  ixxss2  12747  ixxss12  12748  ixxub  12749  ixxlb  12750  lbioo  12759  elicore  12779  iccsupr  12820  icodisj  12852  xov1plusxeqvd  12874  intfracq  13217  fldiv  13218  seqf1olem2  13400  cjmul  14491  icco1  14887  sumtp  15094  rpnnen2lem10  15566  ruclem2  15575  ruclem3  15576  ruclem9  15581  ruclem12  15584  dvdslegcd  15843  crth  16105  eulerthlem1  16108  eulerthlem2  16109  pcpremul  16170  prmreclem2  16243  prmreclem3  16244  4sqlem13  16283  sectcan  17015  sectco  17016  sectmon  17042  monsect  17043  funcid  17130  funcco  17131  funcsect  17132  invfuc  17234  fuciso  17235  coapm  17321  catciso  17357  postr  17553  ipodrsima  17765  psref2  17804  psasym  17810  mhm0  17954  submcl  17967  submmnd  17968  eqger  18270  eqgcpbl  18274  gaorber  18378  orbsta  18383  cayleyth  18474  pmtrrn2  18519  pmtrfinv  18520  pmtrfmvdn0  18521  dfod2  18622  sylow2blem1  18676  sylow2blem3  18678  dprdcntz  19061  dprddisj  19062  dprdffsupp  19067  dpjdisj  19106  ablfac1a  19122  ablfac1b  19123  lmodvsdir  19589  lmhmlin  19738  lbsind  19783  2idlcpbl  19937  assasca  20024  mpfind  20250  mdetunilem2  21152  mdetunilem5  21155  mdetunilem6  21156  mnfnei  21759  cnprcl  21783  lmcvg  21800  lmff  21839  lmcls  21840  lmcnp  21842  fbasssin  22374  flimfil  22507  tgpconncomp  22650  tlmtrg  22727  ustssel  22743  ustincl  22745  ustdiag  22746  ustinvel  22747  ustexhalf  22748  ustfilxp  22750  tustopn  22809  tususp  22810  imasdsf1olem  22912  xmeter  22972  xmetresbl  22976  tmstopn  23024  metustexhalf  23095  nlmnrg  23217  qdensere  23307  blcvx  23335  tgqioo  23337  icccmplem1  23359  icccmplem2  23360  reconnlem1  23363  cnmpopc  23461  iccpnfcnv  23477  phtpcer  23528  phtpcco2  23532  pcohtpy  23553  pcorev2  23561  pcophtb  23562  om1addcl  23566  pi1blem  23572  pi1cpbl  23577  pi1grplem  23582  pi1inv  23585  pi1xfrf  23586  pi1xfr  23588  pi1xfrcnvlem  23589  pi1cof  23592  pi1coghm  23594  cphreccllem  23711  cphsca  23712  cphsubrg  23713  cphsqrtcl2  23719  phclm  23764  tcphcph  23769  lmmcvg  23793  cmetcaulem  23820  lmcau  23845  bcthlem3  23858  bcthlem4  23859  minveclem4c  23957  minveclem2  23958  minveclem3b  23960  minveclem4  23964  minveclem6  23966  ivthicc  23988  ovollb2lem  24018  ovolshftlem1  24039  ovolscalem1  24043  ovolicc1  24046  ovolicc2lem2  24048  ovolicc2lem3  24049  ovolicc2lem4  24050  ovolicc2lem5  24051  ioombl1lem1  24088  dyadmaxlem  24127  volivth  24137  vitalilem2  24139  vitalilem4  24141  i1fima2  24209  itg2monolem1  24280  itgcnlem  24319  itgrevallem1  24324  itgreval  24326  itgle  24339  ibladd  24350  iblabslem  24357  itgspliticc  24366  itgsplitioo  24367  ditgcl  24385  ditgswap  24386  ditgsplitlem  24387  limcdif  24403  limcresi  24412  limcres  24413  limccnp  24418  limccnp2  24419  limcun  24422  dvlip  24519  dvlip2  24521  dveq0  24526  dvgt0lem1  24528  dvivthlem1  24534  dvcnvrelem1  24543  dvcnvre  24545  dvfsumlem2  24553  ftc1lem1  24561  ftc1lem2  24562  ftc1a  24563  ftc1lem4  24565  ftc2  24570  ftc2ditglem  24571  itgsubstlem  24574  ply1rem  24686  fta1glem2  24689  ig1pdvds  24699  plyrem  24823  fta1lem  24825  vieta1lem2  24829  aaliou3lem3  24862  pserulm  24939  psercnlem2  24941  psercnlem1  24942  psercn  24943  pserdvlem1  24944  pserdvlem2  24945  abelth2  24959  coseq00topi  25017  coseq0negpitopi  25018  cosordlem  25042  tanord1  25048  efif1olem1  25053  dvloglem  25158  efopnlem1  25166  logreclem  25267  relogbval  25277  nnlogbexp  25286  logbrec  25287  chordthmlem4  25340  quart1  25361  quartlem2  25363  quartlem3  25364  quart  25366  acosbnd  25405  atancj  25415  atanlogsublem  25420  atantan  25428  atanbndlem  25430  atans2  25436  dvatan  25440  atantayl  25442  divsqrtsumlem  25485  ftalem5  25582  basellem5  25590  ppisval  25609  chtleppi  25714  chpchtsum  25723  chpub  25724  mersenne  25731  perfectlem2  25734  dchrinv  25765  rplogsumlem2  25989  chpdifbndlem1  26057  pntibndlem2  26095  pntlema  26100  pntlemb  26101  pntlemg  26102  pntlemh  26103  pntlemr  26106  pntlemj  26107  pntlemf  26109  pntlemk  26110  pntlemo  26111  pntlemp  26114  pntleml  26115  abvcxp  26119  ostth2lem2  26138  axtgcont1  26182  cgr3simp3  26236  legso  26313  hlln  26321  hltr  26324  btwnhl  26328  mirhl  26393  mirbtwnhl  26394  opphllem4  26464  opphl  26468  hlpasch  26470  cgracgr  26532  cgraswap  26534  cgrahl  26541  cgracol  26542  inagswap  26555  inagne3  26558  dfcgrg2  26577  umgrnloopv  26819  umgredgne  26858  usgrnloopvALT  26911  frusgrnn0  27281  cusgrm1rusgr  27292  upgrclwlkcompim  27490  2wlkdlem6  27638  2wlkond  27644  2trlond  27646  numclwwlk2lem1  28083  numclwlk2lem2f1o  28086  tncp  28183  grpolidinv  28206  nvs  28368  nvz  28374  nvtri  28375  sspn  28441  minvecolem2  28580  minvecolem4c  28584  minvecolem4  28585  minvecolem5  28586  minvecolem6  28587  adj1  29638  eliccelico  30427  elicoelioo  30428  prmdvdsbc  30459  pmtrto1cl  30669  cyc3evpm  30720  slmdvsdir  30772  slmd0vs  30780  prmidl  30877  qsidomlem2  30884  locfinreflem  31004  cnre2csqlem  31053  sigaclci  31291  unelsiga  31293  insiga  31296  unelldsys  31317  ldsysgenld  31319  sigapildsys  31321  ldgenpisyslem1  31322  measvun  31368  cntmeas  31385  sibfima  31496  signstfveq0  31747  tg5segofs  31844  bnj1018  32134  pfxwlk  32268  revwlk  32269  spthcycl  32274  acycgrcycl  32292  subfacp1lem3  32327  subfacp1lem4  32328  subfacp1lem5  32329  sconnpht2  32383  sconnpi1  32384  txsconn  32386  resconn  32391  cvmcn  32407  cvmsuni  32414  cvmsdisj  32415  cvmshmeo  32416  cvmlift2lem8  32455  cvmlift2lem13  32460  cvmliftphtlem  32462  cvmliftpht  32463  cvmlift3lem6  32469  msrf  32687  elmsta  32693  mthmpps  32727  mclsppslem  32728  scutun12  33169  slerec  33175  ivthALT  33581  relowlssretop  34527  ibladdnc  34831  iblabsnclem  34837  ftc2nc  34858  dvasin  34860  isbndx  34943  isbnd3  34945  prdsbnd  34954  heiborlem3  34974  iccbnd  35001  rngohomadd  35130  rngohommul  35131  idladdcl  35180  idllmulcl  35181  idlrmulcl  35182  maxidlmax  35204  pridlc  35232  eqvreltr  35724  lshpnelb  36002  lshpcmp  36006  oplecon3  36217  opnoncon  36226  hlcvl  36377  dochshpncl  38402  lclkrslem1  38555  lclkrslem2  38556  acongrep  39457  ntrneinex  40307  neicvgmex  40347  gneispace0nelrn  40370  cvgdvgrat  40525  binomcxplemdvbinom  40565  eliocre  41665  iccshift  41674  iccsuble  41675  icoiccdif  41680  mullimc  41777  limccog  41781  limciccioolb  41782  mullimcf  41784  limcperiod  41789  lptioo2  41792  lptioo1  41793  neglimc  41808  addlimc  41809  0ellimcdiv  41810  reclimc  41814  xlimmnfvlem1  41993  xlimpnfvlem1  41997  icccncfext  42050  cncfioobdlem  42059  ditgeqiooicc  42125  iblspltprt  42138  iblcncfioo  42143  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem11  42177  stoweidlem31  42197  stoweidlem36  42202  stoweidlem38  42204  stoweidlem62  42228  dirkercncflem1  42269  dirkercncflem4  42272  fourierdlem26  42299  fourierdlem32  42305  fourierdlem33  42306  fourierdlem37  42310  fourierdlem42  42315  fourierdlem54  42326  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem74  42346  fourierdlem75  42347  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem93  42365  fourierdlem101  42373  fourierdlem107  42379  fourierdlem109  42381  fourierdlem111  42383  salunicl  42482  saluncl  42483  hoidmv1lelem1  42754  hoidmv1lelem3  42756  hoidmvlelem1  42758  ovolval3  42810  iinhoiicclem  42836  smfpreimalt  42889  smfpreimaltf  42894  smfpreimale  42912  issmfgt  42914  smfpreimagt  42919  smfpreimage  42939  sigardiv  42999  sigarcol  43002  sharhght  43003  sigaradd  43004  cevathlem1  43005  cevathlem2  43006  cevath  43007  proththd  43626  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator