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

Theorem simp1d 1066
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 1054 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  simp1bi  1069  f1dom3fv3dif  6425  f1dom3el3dif  6426  f1prex  6439  oeeui  7569  oeeu  7570  erinxp  7708  domssex2  8005  domssex  8006  cantnflem1a  8465  cantnflem1b  8466  cantnflem1c  8467  cantnflem1d  8468  cantnflem1  8469  cantnflem3  8471  cantnflem4  8472  fpwwe2lem7  9337  canthnumlem  9349  canthp1lem2  9354  wuntr  9406  lelttrdi  10078  supmul1  10869  supmullem1  10870  supmullem2  10871  supmul  10872  ixxdisj  12061  ixxun  12062  ixxss1  12064  ixxss2  12065  ixxss12  12066  ixxub  12067  ixxlb  12068  iccss2  12115  iocssre  12124  icossre  12125  iccssre  12126  icodisj  12168  iccf1o  12187  xov1plusxeqvd  12189  fzen  12229  intfracq  12520  fldiv  12521  remul  13717  sqrlem6  13836  resqrtth  13844  sqrtth  13952  ruclem6  14803  ruclem9  14806  ruclem12  14809  gcdn0cl  15062  crth  15321  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  pcpremul  15386  prmreclem3  15460  sectcan  16238  sectco  16239  sectmon  16265  monsect  16266  funcf1  16349  funcsect  16355  invfuc  16457  coapm  16544  catciso  16580  psrel  17026  pstr  17034  mhmf  17163  submss  17173  eqger  17467  eqgcpbl  17471  gaorber  17564  orbstafun  17567  cayleyth  17658  dprdgrp  18227  dprdff  18234  ablfac1a  18291  ablfac1b  18292  lmodvscl  18703  lbsss  18898  2idlcpbl  19055  assalmod  19140  mpfind  19357  mdetunilem2  20238  mdetunilem5  20241  mdetunilem6  20242  chfacfisfcpmat  20479  cnptop1  20856  lmfpm  20909  lmff  20915  lmcnp  20918  flimtop  21579  tlmtmd  21800  ustssxp  21818  ustdiag  21822  ustfilxp  21826  ustbas2  21839  tusbas  21882  imasdsf1olem  21988  xmeter  22048  tmsbas  22098  metustexhalf  22171  nlmngp  22291  qdensere  22383  blcvx  22409  tgqioo  22411  icccmplem2  22434  reconnlem1  22437  cnmpt2pc  22535  icoopnst  22546  iocopnst  22547  iccpnfcnv  22551  phtpcer  22602  phtpcerOLD  22603  phtpcco2  22607  pcohtpylem  22627  pcohtpy  22628  pcopt  22630  pcopt2  22631  pcorevlem  22634  pcorev2  22636  pcophtb  22637  om1addcl  22641  pi1cpbl  22652  pi1grplem  22657  pi1inv  22660  pi1xfrf  22661  pi1xfr  22663  pi1xfrcnvlem  22664  pi1xfrcnv  22665  pi1cof  22667  pi1coghm  22669  cphphl  22779  cphreccllem  22786  cphsqrtcl2  22794  tchclm  22839  tchcph  22844  lmcau  22919  bcthlem4  22932  minveclem4c  23004  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  ivthicc  23034  ovolfsval  23046  ovollb2lem  23063  ovolshftlem1  23084  ovolscalem1  23088  ovolicc2lem2  23093  ovolicc2lem5  23096  ovolicopnf  23099  ioombl1lem1  23133  ioombl1lem3  23135  ioombl1lem4  23136  uniioovol  23153  uniioombllem2a  23156  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  vitalilem2  23184  vitalilem3  23185  vitalilem4  23186  i1ff  23249  itg2monolem1  23323  itgreval  23369  ibladd  23393  iblabslem  23400  itgspliticc  23409  itgsplitioo  23410  ditgcl  23428  ditgswap  23429  ditgsplitlem  23430  ditgsplit  23431  limcresi  23455  dvlip2  23562  dveq0  23567  dvcnvre  23586  dvfsumlem2  23594  ftc1a  23604  ply1rem  23727  facth1  23728  fta1glem1  23729  fta1glem2  23730  ig1pcl  23739  ig1pdvds  23740  plyrem  23864  facth  23865  vieta1lem1  23869  vieta1lem2  23870  aaliou3lem3  23903  aaliou3lem7  23908  pserulm  23980  psercnlem2  23982  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  abelth2  24000  coseq00topi  24058  coseq0negpitopi  24059  cosordlem  24081  efif1olem1  24092  dvloglem  24194  loglesqrt  24299  relogbval  24310  nnlogbexp  24319  logbrec  24320  quart1  24383  quartlem2  24385  quartlem3  24386  quartlem4  24387  quart  24388  asinsinlem  24418  atanlogsublem  24442  atans2  24458  dvatan  24462  rlimcnp2  24493  divsqrtsumlem  24506  ftalem5  24603  ftalem7  24605  basellem4  24610  basellem5  24611  perfectlem2  24755  dchrinv  24786  chpdifbndlem1  25042  pntibndlem2  25080  pntlema  25085  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemn  25089  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntlemp  25099  pntleml  25100  abvcxp  25104  axtgbtwnid  25165  cgr3simp1  25215  hlne1  25300  hltr  25305  btwnhl  25309  mirhl  25374  opphllem4  25442  hlpasch  25448  inagswap  25530  wwlksubclwwlk  26332  clwwnisshclwwn  26337  rusisusgra  26458  eupacl  26496  grpofo  26737  vcablo  26808  nvvc  26854  sspba  26966  sspg  26967  minvecolem2  27115  minvecolem4c  27119  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  eleigveccl  28202  xrofsup  28923  eliccelico  28929  elicoelioo  28930  slmdvscl  29098  slmdvsass  29101  baselsiga  29505  insiga  29527  ldsysgenld  29550  sigapildsys  29552  ldgenpisyslem1  29553  measfrge0  29593  sibfmbl  29724  eulerpartlemt  29760  eulerpartlemmf  29764  probfinmeasbOLD  29817  tg5segofs  30004  subfacp1lem2a  30416  subfacp1lem2b  30417  subfacp1lem3  30418  subfacp1lem4  30419  subfacp1lem5  30420  sconpht2  30474  sconpi1  30475  cvxscon  30479  cvmlift2lem3  30541  cvmlift2lem5  30543  cvmlift2lem6  30544  cvmlift2lem7  30545  cvmlift2lem12  30550  cvmliftphtlem  30553  cvmliftpht  30554  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem5  30559  cvmlift3lem6  30560  msrf  30693  elmsta  30699  mthmpps  30733  mclsppslem  30734  mclspps  30735  iblabsnclem  32643  dvasin  32666  isbnd3  32753  heiborlem3  32782  iccbnd  32809  rngohomf  32935  idlss  32985  lshplss  33286  opoccl  33499  opococ  33500  oplecon3  33504  hloml  33662  lclkrslem1  35844  lclkrslem2  35845  eliccre  38575  eliocre  38581  icoiccdif  38597  limccog  38687  lptioo1  38699  cncfiooicclem1  38779  cncfioobdlem  38782  ditgeqiooicc  38852  stoweidlem30  38923  stoweidlem31  38924  stoweidlem38  38931  stoweidlem44  38937  fourierdlem26  39026  fourierdlem32  39032  fourierdlem33  39033  fourierdlem37  39037  fourierdlem42  39042  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem69  39068  fourierdlem79  39078  fourierdlem82  39081  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem111  39110  0sal  39216  hoidmv1lelem3  39483  smfdmss  39619  smfpimltxr  39634  sigardiv  39699  sigarcol  39702  sharhght  39703  sigaradd  39704  cevathlem1  39705  cevathlem2  39706  cevath  39707  proththd  40069  perfectALTVlem2  40165  1wlk1ewlk  40844  1wlkvtxedg  40852  crctcsh1wlkn0  41024  21wlkdlem6  41138  21wlkond  41144  2trlond  41146
  Copyright terms: Public domain W3C validator