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

Theorem simp1d 1139
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 1133 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  simp1bi  1142  f1dom3fv3dif  7018  f1dom3el3dif  7019  f1prex  7032  oeeui  8224  oeeu  8225  domssex2  8674  domssex  8675  cantnflem1a  9145  cantnflem1b  9146  cantnflem1c  9147  cantnflem1d  9148  cantnflem1  9149  cantnflem3  9151  cantnflem4  9152  fpwwe2lem7  10056  canthnumlem  10068  canthp1lem2  10073  wuntr  10125  lelttrdi  10800  supmul1  11606  supmullem1  11607  supmullem2  11608  supmul  11609  ixxdisj  12750  ixxun  12751  ixxss1  12753  ixxss2  12754  ixxss12  12755  ixxub  12756  ixxlb  12757  iccss2  12805  iocssre  12814  icossre  12815  iccssre  12816  icodisj  12863  iccf1o  12883  xov1plusxeqvd  12885  fzen  12928  intfracq  13231  fldiv  13232  remul  14488  sqrlem6  14607  resqrtth  14615  sqrtth  14724  ruclem6  15588  ruclem9  15591  ruclem12  15594  gcdn0cl  15849  crth  16113  phimullem  16114  eulerthlem1  16116  eulerthlem2  16117  pcpremul  16178  prmreclem3  16252  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcf1  17136  funcsect  17142  invfuc  17244  coapm  17331  catciso  17367  psrel  17813  pstr  17821  mhmf  17961  submss  17974  eqger  18330  eqgcpbl  18334  gaorber  18438  orbstafun  18441  cayleyth  18543  dprdgrp  19127  dprdff  19134  ablfac1a  19191  ablfac1b  19192  lmodvscl  19651  lbsss  19849  2idlcpbl  20007  assalmod  20092  mpfind  20320  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  chfacfisfcpmat  21463  cnptop1  21850  lmfpm  21903  lmff  21909  lmcnp  21912  flimtop  22573  tlmtmd  22795  ustssxp  22813  ustdiag  22817  ustfilxp  22821  ustbas2  22834  tusbas  22877  imasdsf1olem  22983  xmeter  23043  tmsbas  23093  metustexhalf  23166  nlmngp  23286  qdensere  23378  blcvx  23406  tgqioo  23408  icccmplem2  23431  reconnlem1  23434  cnmpopc  23536  icoopnst  23547  iocopnst  23548  iccpnfcnv  23552  phtpcer  23603  phtpcco2  23607  pcohtpylem  23627  pcohtpy  23628  pcopt  23630  pcopt2  23631  pcorevlem  23634  pcorev2  23636  pcophtb  23637  om1addcl  23641  pi1grplem  23657  pi1inv  23660  pi1xfrf  23661  pi1xfr  23663  pi1xfrcnvlem  23664  pi1xfrcnv  23665  pi1cof  23667  pi1coghm  23669  cphphl  23779  cphreccllem  23786  cphsqrtcl2  23794  phclm  23839  tcphcph  23844  lmcau  23920  bcthlem4  23934  minveclem4c  24032  minveclem2  24033  minveclem3b  24035  minveclem4  24039  minveclem6  24041  ivthicc  24065  ovolfsval  24077  ovollb2lem  24095  ovolshftlem1  24116  ovolscalem1  24120  ovolicc2lem2  24125  ovolicc2lem5  24128  ovolicopnf  24131  ioombl1lem1  24165  ioombl1lem3  24167  ioombl1lem4  24168  uniioovol  24186  uniioombllem2a  24189  uniioombllem2  24190  uniioombllem3a  24191  uniioombllem3  24192  uniioombllem4  24193  uniioombllem6  24195  vitalilem2  24216  vitalilem3  24217  vitalilem4  24218  i1ff  24283  itg2monolem1  24357  itgreval  24403  ibladd  24427  iblabslem  24434  itgspliticc  24443  itgsplitioo  24444  ditgcl  24464  ditgswap  24465  ditgsplitlem  24466  ditgsplit  24467  limcresi  24491  dvlip2  24601  dveq0  24606  dvcnvre  24625  dvfsumlem2  24633  ftc1a  24643  ply1rem  24767  facth1  24768  fta1glem1  24769  fta1glem2  24770  ig1pcl  24779  ig1pdvds  24780  plyrem  24904  facth  24905  vieta1lem1  24909  vieta1lem2  24910  aaliou3lem3  24943  aaliou3lem7  24948  pserulm  25020  psercnlem2  25022  psercn  25024  pserdvlem1  25025  pserdvlem2  25026  pserdv  25027  abelth2  25040  coseq00topi  25098  coseq0negpitopi  25099  cosordlem  25125  efif1olem1  25137  dvloglem  25242  loglesqrt  25350  relogbval  25361  nnlogbexp  25370  logbrec  25371  quart1  25445  quartlem2  25447  quartlem3  25448  quartlem4  25449  quart  25450  asinsinlem  25480  atanlogsublem  25504  atans2  25520  dvatan  25524  rlimcnp2  25555  divsqrtsumlem  25568  ftalem5  25665  ftalem7  25667  basellem4  25672  basellem5  25673  perfectlem2  25817  dchrinv  25848  chpdifbndlem1  26140  pntibndlem2  26178  pntlema  26183  pntlemb  26184  pntlemg  26185  pntlemh  26186  pntlemn  26187  pntlemq  26188  pntlemr  26189  pntlemj  26190  pntlemf  26192  pntlemk  26193  pntlemo  26194  pntlemp  26197  pntleml  26198  abvcxp  26202  axtgbtwnid  26263  cgr3simp1  26317  hlne1  26402  hltr  26407  btwnhl  26411  mirhl  26476  opphllem4  26547  hlpasch  26553  inagswap  26638  inagne1  26639  dfcgrg2  26660  wlkf  27407  wlk1ewlk  27432  2wlkdlem6  27720  2wlkond  27726  2trlond  27728  grpofo  28285  vcablo  28355  nvvc  28401  sspba  28513  sspg  28514  minvecolem2  28661  minvecolem4c  28665  minvecolem4  28666  minvecolem5  28667  minvecolem6  28668  eleigveccl  29745  xrofsup  30503  eliccelico  30511  elicoelioo  30512  cyc3evpm  30824  slmdvscl  30874  slmdvsass  30877  imaslmod  30955  prmidlidl  31000  mxidlidl  31013  baselsiga  31431  insiga  31453  ldsysgenld  31476  sigapildsys  31478  ldgenpisyslem1  31479  measfrge0  31519  sibfmbl  31650  eulerpartlemt  31686  eulerpartlemmf  31690  probfinmeasbALTV  31744  tg5segofs  32001  pfxwlk  32427  revwlk  32428  subgrwlk  32436  subfacp1lem2a  32484  subfacp1lem2b  32485  subfacp1lem3  32486  subfacp1lem4  32487  subfacp1lem5  32488  sconnpht2  32542  sconnpi1  32543  cvxsconn  32547  cvmlift2lem3  32609  cvmlift2lem5  32611  cvmlift2lem6  32612  cvmlift2lem7  32613  cvmlift2lem12  32618  cvmliftphtlem  32621  cvmliftpht  32622  cvmlift3lem2  32624  cvmlift3lem4  32626  cvmlift3lem5  32627  cvmlift3lem6  32628  msrf  32846  elmsta  32852  mthmpps  32886  mclsppslem  32887  mclspps  32888  scutun12  33328  scutf  33330  slerec  33334  sltrec  33335  madeval2  33347  iblabsnclem  35065  dvasin  35086  isbnd3  35167  heiborlem3  35196  iccbnd  35223  rngohomf  35349  idlss  35399  lshplss  36222  opoccl  36435  opococ  36436  oplecon3  36440  hloml  36598  lclkrslem1  38778  lclkrslem2  38779  metakunt8  39303  metakunt19  39314  metakunt21  39316  metakunt22  39317  metakunt25  39320  eliccre  42068  eliocre  42072  icoiccdif  42087  limccog  42188  lptioo1  42200  cncfiooicclem1  42461  ditgeqiooicc  42528  stoweidlem30  42598  stoweidlem31  42599  stoweidlem38  42606  stoweidlem44  42612  fourierdlem26  42701  fourierdlem32  42707  fourierdlem33  42708  fourierdlem37  42712  fourierdlem42  42717  fourierdlem54  42728  fourierdlem63  42737  fourierdlem64  42738  fourierdlem65  42739  fourierdlem69  42743  fourierdlem79  42753  fourierdlem82  42756  fourierdlem89  42763  fourierdlem90  42764  fourierdlem91  42765  fourierdlem111  42785  0sal  42888  hoidmv1lelem3  43158  smfdmss  43293  smfpimltxr  43307  sigardiv  43401  sigarcol  43404  sharhght  43405  sigaradd  43406  cevathlem1  43407  cevathlem2  43408  cevath  43409  proththd  44058  perfectALTVlem2  44166  itsclc0yqsol  45104
  Copyright terms: Public domain W3C validator