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

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

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp1 1053 . 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:  simp1bi  1068  f1dom3fv3dif  6399  f1dom3el3dif  6400  f1prex  6413  oeeui  7542  oeeu  7543  erinxp  7681  domssex2  7978  domssex  7979  cantnflem1a  8438  cantnflem1b  8439  cantnflem1c  8440  cantnflem1d  8441  cantnflem1  8442  cantnflem3  8444  cantnflem4  8445  fpwwe2lem7  9310  canthnumlem  9322  canthp1lem2  9327  wuntr  9379  lelttrdi  10046  supmul1  10835  supmullem1  10836  supmullem2  10837  supmul  10838  ixxdisj  12013  ixxun  12014  ixxss1  12016  ixxss2  12017  ixxss12  12018  ixxub  12019  ixxlb  12020  iccss2  12067  iocssre  12076  icossre  12077  iccssre  12078  icodisj  12120  iccf1o  12139  xov1plusxeqvd  12141  fzen  12180  intfracq  12471  fldiv  12472  remul  13659  sqrlem6  13778  resqrtth  13786  sqrtth  13894  ruclem6  14745  ruclem9  14748  ruclem12  14751  gcdn0cl  15004  crth  15263  phimullem  15264  eulerthlem1  15266  eulerthlem2  15267  pcpremul  15328  prmreclem3  15402  sectcan  16180  sectco  16181  sectmon  16207  monsect  16208  funcf1  16291  funcsect  16297  invfuc  16399  coapm  16486  catciso  16522  psrel  16968  pstr  16976  mhmf  17105  submss  17115  eqger  17409  eqgcpbl  17413  gaorber  17506  orbstafun  17509  cayleyth  17600  dprdgrp  18169  dprdff  18176  ablfac1a  18233  ablfac1b  18234  lmodvscl  18645  lbsss  18840  2idlcpbl  18997  assalmod  19082  mpfind  19299  mdetunilem2  20176  mdetunilem5  20179  mdetunilem6  20180  chfacfisfcpmat  20417  cnptop1  20794  lmfpm  20847  lmff  20853  lmcnp  20856  flimtop  21517  tlmtmd  21738  ustssxp  21756  ustdiag  21760  ustfilxp  21764  ustbas2  21777  tusbas  21820  imasdsf1olem  21925  xmeter  21985  tmsbas  22035  metustexhalf  22108  nlmngp  22220  qdensere  22311  blcvx  22337  tgqioo  22339  icccmplem2  22362  reconnlem1  22365  cnmpt2pc  22462  icoopnst  22473  iocopnst  22474  iccpnfcnv  22478  phtpcer  22529  phtpcerOLD  22530  phtpcco2  22534  pcohtpylem  22554  pcohtpy  22555  pcopt  22557  pcopt2  22558  pcorevlem  22561  pcorev2  22563  pcophtb  22564  om1addcl  22568  pi1cpbl  22579  pi1grplem  22584  pi1inv  22587  pi1xfrf  22588  pi1xfr  22590  pi1xfrcnvlem  22591  pi1xfrcnv  22592  pi1cof  22594  pi1coghm  22596  cphphl  22699  cphreccllem  22706  cphsqrtcl2  22714  tchclm  22756  tchcph  22761  lmcau  22832  bcthlem4  22845  minveclem4c  22917  minveclem2  22918  minveclem3b  22920  minveclem4  22924  minveclem6  22926  ivthicc  22947  ovolfsval  22959  ovollb2lem  22976  ovolshftlem1  22997  ovolscalem1  23001  ovolicc2lem2  23006  ovolicc2lem5  23009  ovolicopnf  23012  ioombl1lem1  23046  ioombl1lem3  23048  ioombl1lem4  23049  uniioovol  23066  uniioombllem2a  23069  uniioombllem2  23070  uniioombllem3a  23071  uniioombllem3  23072  uniioombllem4  23073  uniioombllem6  23075  vitalilem2  23097  vitalilem3  23098  vitalilem4  23099  i1ff  23162  itg2monolem1  23236  itgreval  23282  ibladd  23306  iblabslem  23313  itgspliticc  23322  itgsplitioo  23323  ditgcl  23341  ditgswap  23342  ditgsplitlem  23343  ditgsplit  23344  limcresi  23368  dvlip2  23475  dveq0  23480  dvcnvre  23499  dvfsumlem2  23507  ftc1a  23517  ply1rem  23640  facth1  23641  fta1glem1  23642  fta1glem2  23643  ig1pcl  23652  ig1pdvds  23653  plyrem  23777  facth  23778  vieta1lem1  23782  vieta1lem2  23783  aaliou3lem3  23816  aaliou3lem7  23821  pserulm  23893  psercnlem2  23895  psercn  23897  pserdvlem1  23898  pserdvlem2  23899  pserdv  23900  abelth2  23913  coseq00topi  23971  coseq0negpitopi  23972  cosordlem  23994  efif1olem1  24005  dvloglem  24107  loglesqrt  24212  relogbval  24223  nnlogbexp  24232  logbrec  24233  quart1  24296  quartlem2  24298  quartlem3  24299  quartlem4  24300  quart  24301  asinsinlem  24331  atanlogsublem  24355  atans2  24371  dvatan  24375  rlimcnp2  24406  divsqrtsumlem  24419  ftalem5  24516  ftalem7  24518  basellem4  24523  basellem5  24524  perfectlem2  24668  dchrinv  24699  chpdifbndlem1  24955  pntibndlem2  24993  pntlema  24998  pntlemb  24999  pntlemg  25000  pntlemh  25001  pntlemn  25002  pntlemq  25003  pntlemr  25004  pntlemj  25005  pntlemf  25007  pntlemk  25008  pntlemo  25009  pntlemp  25012  pntleml  25013  abvcxp  25017  axtgbtwnid  25078  cgr3simp1  25129  hlne1  25214  hltr  25219  btwnhl  25223  mirhl  25288  opphllem4  25356  hlpasch  25362  inagswap  25444  wwlksubclwwlk  26094  clwwnisshclwwn  26099  rusisusgra  26220  eupacl  26258  grpofo  26499  vcablo  26574  nvvc  26634  sspba  26766  sspg  26767  minvecolem2  26917  minvecolem4c  26921  minvecolem4  26922  minvecolem5  26923  minvecolem6  26924  eleigveccl  28004  xrofsup  28725  eliccelico  28731  elicoelioo  28732  slmdvscl  28900  slmdvsass  28903  baselsiga  29307  insiga  29329  ldsysgenld  29352  sigapildsys  29354  ldgenpisyslem1  29355  measfrge0  29395  sibfmbl  29526  eulerpartlemt  29562  eulerpartlemmf  29566  probfinmeasbOLD  29619  tg5segofs  29806  subfacp1lem2a  30218  subfacp1lem2b  30219  subfacp1lem3  30220  subfacp1lem4  30221  subfacp1lem5  30222  sconpht2  30276  sconpi1  30277  cvxscon  30281  cvmlift2lem3  30343  cvmlift2lem5  30345  cvmlift2lem6  30346  cvmlift2lem7  30347  cvmlift2lem12  30352  cvmliftphtlem  30355  cvmliftpht  30356  cvmlift3lem2  30358  cvmlift3lem4  30360  cvmlift3lem5  30361  cvmlift3lem6  30362  msrf  30495  elmsta  30501  mthmpps  30535  mclsppslem  30536  mclspps  30537  iblabsnclem  32442  dvasin  32465  isbnd3  32552  heiborlem3  32581  iccbnd  32608  rngohomf  32734  idlss  32784  lshplss  33085  opoccl  33298  opococ  33299  oplecon3  33303  hloml  33461  lclkrslem1  35643  lclkrslem2  35644  eliccre  38375  eliocre  38381  icoiccdif  38397  limccog  38487  lptioo1  38499  cncfiooicclem1  38579  cncfioobdlem  38582  ditgeqiooicc  38652  stoweidlem30  38723  stoweidlem31  38724  stoweidlem38  38731  stoweidlem44  38737  fourierdlem26  38826  fourierdlem32  38832  fourierdlem33  38833  fourierdlem37  38837  fourierdlem42  38842  fourierdlem54  38853  fourierdlem63  38862  fourierdlem64  38863  fourierdlem65  38864  fourierdlem69  38868  fourierdlem79  38878  fourierdlem82  38881  fourierdlem89  38888  fourierdlem90  38889  fourierdlem91  38890  fourierdlem111  38910  0sal  39016  hoidmv1lelem3  39283  smfdmss  39419  smfpimltxr  39434  sigardiv  39499  sigarcol  39502  sharhght  39503  sigaradd  39504  cevathlem1  39505  cevathlem2  39506  cevath  39507  proththd  39870  perfectALTVlem2  39966  1wlk1ewlk  40842  1wlkvtxedg  40850  crctcsh1wlkn0  41022  21wlkdlem6  41136  21wlkond  41142  2trlond  41144
  Copyright terms: Public domain W3C validator