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

Theorem simp1d 1071
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 1059 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1036
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 197  df-an 386  df-3an 1038
This theorem is referenced by:  simp1bi  1074  f1dom3fv3dif  6510  f1dom3el3dif  6511  f1prex  6524  oeeui  7667  oeeu  7668  erinxp  7806  domssex2  8105  domssex  8106  cantnflem1a  8567  cantnflem1b  8568  cantnflem1c  8569  cantnflem1d  8570  cantnflem1  8571  cantnflem3  8573  cantnflem4  8574  fpwwe2lem7  9443  canthnumlem  9455  canthp1lem2  9460  wuntr  9512  lelttrdi  10184  supmul1  10977  supmullem1  10978  supmullem2  10979  supmul  10980  ixxdisj  12175  ixxun  12176  ixxss1  12178  ixxss2  12179  ixxss12  12180  ixxub  12181  ixxlb  12182  iccss2  12229  iocssre  12238  icossre  12239  iccssre  12240  icodisj  12282  iccf1o  12301  xov1plusxeqvd  12303  fzen  12343  intfracq  12641  fldiv  12642  remul  13850  sqrlem6  13969  resqrtth  13977  sqrtth  14085  ruclem6  14945  ruclem9  14948  ruclem12  14951  gcdn0cl  15205  crth  15464  phimullem  15465  eulerthlem1  15467  eulerthlem2  15468  pcpremul  15529  prmreclem3  15603  sectcan  16396  sectco  16397  sectmon  16423  monsect  16424  funcf1  16507  funcsect  16513  invfuc  16615  coapm  16702  catciso  16738  psrel  17184  pstr  17192  mhmf  17321  submss  17331  eqger  17625  eqgcpbl  17629  gaorber  17722  orbstafun  17725  cayleyth  17816  dprdgrp  18385  dprdff  18392  ablfac1a  18449  ablfac1b  18450  lmodvscl  18861  lbsss  19058  2idlcpbl  19215  assalmod  19300  mpfind  19517  mdetunilem2  20400  mdetunilem5  20403  mdetunilem6  20404  chfacfisfcpmat  20641  cnptop1  21027  lmfpm  21080  lmff  21086  lmcnp  21089  flimtop  21750  tlmtmd  21971  ustssxp  21989  ustdiag  21993  ustfilxp  21997  ustbas2  22010  tusbas  22053  imasdsf1olem  22159  xmeter  22219  tmsbas  22269  metustexhalf  22342  nlmngp  22462  qdensere  22554  blcvx  22582  tgqioo  22584  icccmplem2  22607  reconnlem1  22610  cnmpt2pc  22708  icoopnst  22719  iocopnst  22720  iccpnfcnv  22724  phtpcer  22775  phtpcerOLD  22776  phtpcco2  22780  pcohtpylem  22800  pcohtpy  22801  pcopt  22803  pcopt2  22804  pcorevlem  22807  pcorev2  22809  pcophtb  22810  om1addcl  22814  pi1cpbl  22825  pi1grplem  22830  pi1inv  22833  pi1xfrf  22834  pi1xfr  22836  pi1xfrcnvlem  22837  pi1xfrcnv  22838  pi1cof  22840  pi1coghm  22842  cphphl  22952  cphreccllem  22959  cphsqrtcl2  22967  tchclm  23012  tchcph  23017  lmcau  23092  bcthlem4  23105  minveclem4c  23177  minveclem2  23178  minveclem3b  23180  minveclem4  23184  minveclem6  23186  ivthicc  23208  ovolfsval  23220  ovollb2lem  23237  ovolshftlem1  23258  ovolscalem1  23262  ovolicc2lem2  23267  ovolicc2lem5  23270  ovolicopnf  23273  ioombl1lem1  23307  ioombl1lem3  23309  ioombl1lem4  23310  uniioovol  23328  uniioombllem2a  23331  uniioombllem2  23332  uniioombllem3a  23333  uniioombllem3  23334  uniioombllem4  23335  uniioombllem6  23337  vitalilem2  23359  vitalilem3  23360  vitalilem4  23361  i1ff  23424  itg2monolem1  23498  itgreval  23544  ibladd  23568  iblabslem  23575  itgspliticc  23584  itgsplitioo  23585  ditgcl  23603  ditgswap  23604  ditgsplitlem  23605  ditgsplit  23606  limcresi  23630  dvlip2  23739  dveq0  23744  dvcnvre  23763  dvfsumlem2  23771  ftc1a  23781  ply1rem  23904  facth1  23905  fta1glem1  23906  fta1glem2  23907  ig1pcl  23916  ig1pdvds  23917  plyrem  24041  facth  24042  vieta1lem1  24046  vieta1lem2  24047  aaliou3lem3  24080  aaliou3lem7  24085  pserulm  24157  psercnlem2  24159  psercn  24161  pserdvlem1  24162  pserdvlem2  24163  pserdv  24164  abelth2  24177  coseq00topi  24235  coseq0negpitopi  24236  cosordlem  24258  efif1olem1  24269  dvloglem  24375  loglesqrt  24480  relogbval  24491  nnlogbexp  24500  logbrec  24501  quart1  24564  quartlem2  24566  quartlem3  24567  quartlem4  24568  quart  24569  asinsinlem  24599  atanlogsublem  24623  atans2  24639  dvatan  24643  rlimcnp2  24674  divsqrtsumlem  24687  ftalem5  24784  ftalem7  24786  basellem4  24791  basellem5  24792  perfectlem2  24936  dchrinv  24967  chpdifbndlem1  25223  pntibndlem2  25261  pntlema  25266  pntlemb  25267  pntlemg  25268  pntlemh  25269  pntlemn  25270  pntlemq  25271  pntlemr  25272  pntlemj  25273  pntlemf  25275  pntlemk  25276  pntlemo  25277  pntlemp  25280  pntleml  25281  abvcxp  25285  axtgbtwnid  25346  cgr3simp1  25396  hlne1  25481  hltr  25486  btwnhl  25490  mirhl  25555  opphllem4  25623  hlpasch  25629  inagswap  25711  wlkf  26491  wlk1ewlk  26517  2wlkdlem6  26808  2wlkond  26814  2trlond  26816  grpofo  27323  vcablo  27394  nvvc  27440  sspba  27552  sspg  27553  minvecolem2  27701  minvecolem4c  27705  minvecolem4  27706  minvecolem5  27707  minvecolem6  27708  eleigveccl  28788  xrofsup  29507  eliccelico  29513  elicoelioo  29514  slmdvscl  29741  slmdvsass  29744  baselsiga  30152  insiga  30174  ldsysgenld  30197  sigapildsys  30199  ldgenpisyslem1  30200  measfrge0  30240  sibfmbl  30371  eulerpartlemt  30407  eulerpartlemmf  30411  probfinmeasbOLD  30464  tg5segofs  30725  subfacp1lem2a  31136  subfacp1lem2b  31137  subfacp1lem3  31138  subfacp1lem4  31139  subfacp1lem5  31140  sconnpht2  31194  sconnpi1  31195  cvxsconn  31199  cvmlift2lem3  31261  cvmlift2lem5  31263  cvmlift2lem6  31264  cvmlift2lem7  31265  cvmlift2lem12  31270  cvmliftphtlem  31273  cvmliftpht  31274  cvmlift3lem2  31276  cvmlift3lem4  31278  cvmlift3lem5  31279  cvmlift3lem6  31280  msrf  31413  elmsta  31419  mthmpps  31453  mclsppslem  31454  mclspps  31455  scutun12  31891  scutf  31893  slerec  31897  sltrec  31898  madeval2  31910  iblabsnclem  33444  dvasin  33467  isbnd3  33554  heiborlem3  33583  iccbnd  33610  rngohomf  33736  idlss  33786  lshplss  34087  opoccl  34300  opococ  34301  oplecon3  34305  hloml  34463  lclkrslem1  36645  lclkrslem2  36646  eliccre  39531  eliocre  39537  icoiccdif  39553  limccog  39652  lptioo1  39664  cncfiooicclem1  39869  ditgeqiooicc  39939  stoweidlem30  40010  stoweidlem31  40011  stoweidlem38  40018  stoweidlem44  40024  fourierdlem26  40113  fourierdlem32  40119  fourierdlem33  40120  fourierdlem37  40124  fourierdlem42  40129  fourierdlem54  40140  fourierdlem63  40149  fourierdlem64  40150  fourierdlem65  40151  fourierdlem69  40155  fourierdlem79  40165  fourierdlem82  40168  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem111  40197  0sal  40303  hoidmv1lelem3  40570  smfdmss  40705  smfpimltxr  40719  sigardiv  40813  sigarcol  40816  sharhght  40817  sigaradd  40818  cevathlem1  40819  cevathlem2  40820  cevath  40821  proththd  41296  perfectALTVlem2  41396
  Copyright terms: Public domain W3C validator