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

Theorem simp1d 1134
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 1128 . 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:  simp1bi  1137  f1dom3fv3dif  7017  f1dom3el3dif  7018  f1prex  7031  oeeui  8218  oeeu  8219  domssex2  8666  domssex  8667  cantnflem1a  9137  cantnflem1b  9138  cantnflem1c  9139  cantnflem1d  9140  cantnflem1  9141  cantnflem3  9143  cantnflem4  9144  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wuntr  10116  lelttrdi  10791  supmul1  11599  supmullem1  11600  supmullem2  11601  supmul  11602  ixxdisj  12743  ixxun  12744  ixxss1  12746  ixxss2  12747  ixxss12  12748  ixxub  12749  ixxlb  12750  iccss2  12797  iocssre  12806  icossre  12807  iccssre  12808  icodisj  12852  iccf1o  12872  xov1plusxeqvd  12874  fzen  12914  intfracq  13217  fldiv  13218  remul  14478  sqrlem6  14597  resqrtth  14605  sqrtth  14714  ruclem6  15578  ruclem9  15581  ruclem12  15584  gcdn0cl  15841  crth  16105  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  pcpremul  16170  prmreclem3  16244  sectcan  17015  sectco  17016  sectmon  17042  monsect  17043  funcf1  17126  funcsect  17132  invfuc  17234  coapm  17321  catciso  17357  psrel  17803  pstr  17811  mhmf  17951  submss  17964  eqger  18270  eqgcpbl  18274  gaorber  18378  orbstafun  18381  cayleyth  18474  dprdgrp  19058  dprdff  19065  ablfac1a  19122  ablfac1b  19123  lmodvscl  19582  lbsss  19780  2idlcpbl  19937  assalmod  20022  mpfind  20250  mdetunilem2  21152  mdetunilem5  21155  mdetunilem6  21156  chfacfisfcpmat  21393  cnptop1  21780  lmfpm  21833  lmff  21839  lmcnp  21842  flimtop  22503  tlmtmd  22724  ustssxp  22742  ustdiag  22746  ustfilxp  22750  ustbas2  22763  tusbas  22806  imasdsf1olem  22912  xmeter  22972  tmsbas  23022  metustexhalf  23095  nlmngp  23215  qdensere  23307  blcvx  23335  tgqioo  23337  icccmplem2  23360  reconnlem1  23363  cnmpopc  23461  icoopnst  23472  iocopnst  23473  iccpnfcnv  23477  phtpcer  23528  phtpcco2  23532  pcohtpylem  23552  pcohtpy  23553  pcopt  23555  pcopt2  23556  pcorevlem  23559  pcorev2  23561  pcophtb  23562  om1addcl  23566  pi1grplem  23582  pi1inv  23585  pi1xfrf  23586  pi1xfr  23588  pi1xfrcnvlem  23589  pi1xfrcnv  23590  pi1cof  23592  pi1coghm  23594  cphphl  23704  cphreccllem  23711  cphsqrtcl2  23719  phclm  23764  tcphcph  23769  lmcau  23845  bcthlem4  23859  minveclem4c  23957  minveclem2  23958  minveclem3b  23960  minveclem4  23964  minveclem6  23966  ivthicc  23988  ovolfsval  24000  ovollb2lem  24018  ovolshftlem1  24039  ovolscalem1  24043  ovolicc2lem2  24048  ovolicc2lem5  24051  ovolicopnf  24054  ioombl1lem1  24088  ioombl1lem3  24090  ioombl1lem4  24091  uniioovol  24109  uniioombllem2a  24112  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem6  24118  vitalilem2  24139  vitalilem3  24140  vitalilem4  24141  i1ff  24206  itg2monolem1  24280  itgreval  24326  ibladd  24350  iblabslem  24357  itgspliticc  24366  itgsplitioo  24367  ditgcl  24385  ditgswap  24386  ditgsplitlem  24387  ditgsplit  24388  limcresi  24412  dvlip2  24521  dveq0  24526  dvcnvre  24545  dvfsumlem2  24553  ftc1a  24563  ply1rem  24686  facth1  24687  fta1glem1  24688  fta1glem2  24689  ig1pcl  24698  ig1pdvds  24699  plyrem  24823  facth  24824  vieta1lem1  24828  vieta1lem2  24829  aaliou3lem3  24862  aaliou3lem7  24867  pserulm  24939  psercnlem2  24941  psercn  24943  pserdvlem1  24944  pserdvlem2  24945  pserdv  24946  abelth2  24959  coseq00topi  25017  coseq0negpitopi  25018  cosordlem  25042  efif1olem1  25053  dvloglem  25158  loglesqrt  25266  relogbval  25277  nnlogbexp  25286  logbrec  25287  quart1  25361  quartlem2  25363  quartlem3  25364  quartlem4  25365  quart  25366  asinsinlem  25396  atanlogsublem  25420  atans2  25436  dvatan  25440  rlimcnp2  25472  divsqrtsumlem  25485  ftalem5  25582  ftalem7  25584  basellem4  25589  basellem5  25590  perfectlem2  25734  dchrinv  25765  chpdifbndlem1  26057  pntibndlem2  26095  pntlema  26100  pntlemb  26101  pntlemg  26102  pntlemh  26103  pntlemn  26104  pntlemq  26105  pntlemr  26106  pntlemj  26107  pntlemf  26109  pntlemk  26110  pntlemo  26111  pntlemp  26114  pntleml  26115  abvcxp  26119  axtgbtwnid  26180  cgr3simp1  26234  hlne1  26319  hltr  26324  btwnhl  26328  mirhl  26393  opphllem4  26464  hlpasch  26470  inagswap  26555  inagne1  26556  dfcgrg2  26577  wlkf  27324  wlk1ewlk  27349  2wlkdlem6  27638  2wlkond  27644  2trlond  27646  grpofo  28204  vcablo  28274  nvvc  28320  sspba  28432  sspg  28433  minvecolem2  28580  minvecolem4c  28584  minvecolem4  28585  minvecolem5  28586  minvecolem6  28587  eleigveccl  29664  xrofsup  30419  eliccelico  30427  elicoelioo  30428  cyc3evpm  30720  slmdvscl  30770  slmdvsass  30773  imaslmod  30850  prmidlidl  30879  baselsiga  31274  insiga  31296  ldsysgenld  31319  sigapildsys  31321  ldgenpisyslem1  31322  measfrge0  31362  sibfmbl  31493  eulerpartlemt  31529  eulerpartlemmf  31533  probfinmeasbALTV  31587  tg5segofs  31844  pfxwlk  32268  revwlk  32269  subgrwlk  32277  subfacp1lem2a  32325  subfacp1lem2b  32326  subfacp1lem3  32327  subfacp1lem4  32328  subfacp1lem5  32329  sconnpht2  32383  sconnpi1  32384  cvxsconn  32388  cvmlift2lem3  32450  cvmlift2lem5  32452  cvmlift2lem6  32453  cvmlift2lem7  32454  cvmlift2lem12  32459  cvmliftphtlem  32462  cvmliftpht  32463  cvmlift3lem2  32465  cvmlift3lem4  32467  cvmlift3lem5  32468  cvmlift3lem6  32469  msrf  32687  elmsta  32693  mthmpps  32727  mclsppslem  32728  mclspps  32729  scutun12  33169  scutf  33171  slerec  33175  sltrec  33176  madeval2  33188  iblabsnclem  34837  dvasin  34860  isbnd3  34945  heiborlem3  34974  iccbnd  35001  rngohomf  35127  idlss  35177  lshplss  35999  opoccl  36212  opococ  36213  oplecon3  36217  hloml  36375  lclkrslem1  38555  lclkrslem2  38556  eliccre  41661  eliocre  41665  icoiccdif  41680  limccog  41781  lptioo1  41793  cncfiooicclem1  42056  ditgeqiooicc  42125  stoweidlem30  42196  stoweidlem31  42197  stoweidlem38  42204  stoweidlem44  42210  fourierdlem26  42299  fourierdlem32  42305  fourierdlem33  42306  fourierdlem37  42310  fourierdlem42  42315  fourierdlem54  42326  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem69  42341  fourierdlem79  42351  fourierdlem82  42354  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem111  42383  0sal  42486  hoidmv1lelem3  42756  smfdmss  42891  smfpimltxr  42905  sigardiv  42999  sigarcol  43002  sharhght  43003  sigaradd  43004  cevathlem1  43005  cevathlem2  43006  cevath  43007  proththd  43626  perfectALTVlem2  43734  itsclc0yqsol  44649
  Copyright terms: Public domain W3C validator