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

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

Proof of Theorem simp2d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp2 1061 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1037
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 1039
This theorem is referenced by:  simp2bi  1076  f1dom3fv3dif  6522  f1dom3el3dif  6523  f1prex  6536  oeeui  7679  erinxp  7818  resixp  7940  domssex  8118  cantnflem1a  8579  cantnflem1d  8582  cantnflem3  8585  cantnflem4  8586  fpwwe2lem7  9455  canthnumlem  9467  canthp1lem2  9472  wun0  9537  lelttrdi  10196  supmullem2  10991  supmul  10992  ixxdisj  12187  ixxun  12188  ixxss1  12190  ixxss2  12191  ixxss12  12192  ixxub  12193  ixxlb  12194  ubioo  12204  elicore  12223  iccgelb  12227  iccss2  12241  icodisj  12294  xov1plusxeqvd  12315  fldiv  12654  immul  13870  sqrtge0  13992  sqrtrege0  14099  icco1  14265  ruclem2  14955  ruclem3  14956  ruclem8  14960  ruclem12  14964  gcddvds  15219  crth  15477  phimullem  15478  eulerthlem1  15480  eulerthlem2  15481  prmreclem3  15616  sectcan  16409  sectco  16410  sectmon  16436  monsect  16437  funcixp  16521  funcsect  16526  invfuc  16628  coapm  16715  catciso  16751  posasymb  16946  ipodrsima  17159  pstr2  17199  psdmrn  17201  psref  17202  mhmlin  17336  subm0cl  17346  eqger  17638  eqgcpbl  17642  gaorber  17735  orbstafun  17738  cayleyth  17829  pmtrrn2  17874  pmtrfinv  17875  dfod2  17975  sylow2blem1  18029  dprdf  18399  dprdff  18405  dprdfcl  18406  dprdsplit  18441  dpjcntz  18445  ablfac1a  18462  ablfac1b  18463  lmodvsdi  18880  lbssp  19073  2idlcpbl  19228  assaring  19314  mpff  19527  mpfaddcl  19528  mpfmulcl  19529  mpfind  19530  pf1rcl  19707  mpfpf1  19709  mdetunilem2  20413  mdetunilem5  20416  mdetunilem6  20417  chfacfisfcpmat  20654  pnfnei  21018  cnptop2  21041  lmcl  21095  lmcnp  21102  flimfil  21767  tlmlmod  21986  ustbasel  22004  ustincl  22005  ustinvel  22007  ustfilxp  22010  tusunif  22067  imasdsf1olem  22172  xmeter  22232  tmsds  22283  metustexhalf  22355  nlmlmod  22476  qdensere  22567  blcvx  22595  tgqioo  22597  icccmplem2  22620  reconnlem1  22623  cnmpt2pc  22721  phtpcer  22788  phtpcerOLD  22789  phtpcco2  22793  pcohtpylem  22813  pcohtpy  22814  pcophtb  22823  om1addcl  22827  pi1blem  22833  pi1cpbl  22838  pi1grplem  22843  pi1inv  22846  pi1xfrf  22847  pi1xfr  22849  pi1xfrcnvlem  22850  pi1cof  22853  pi1coghm  22855  cphnlm  22966  cphsqrtcl2  22980  tchcph  23030  lmcau  23105  bcthlem4  23118  minveclem4c  23190  minveclem2  23191  minveclem3b  23193  minveclem4  23197  minveclem6  23199  ivthicc  23221  ovolfsval  23233  ovollb2lem  23250  ovolshftlem1  23271  ovolscalem1  23275  ovolicc1  23278  ovolicc2lem2  23280  ovolicc2lem4  23282  ovolicc2lem5  23283  ovolicopnf  23286  ioombl1lem1  23320  ioombl1lem3  23322  ioombl1lem4  23323  uniioovol  23341  uniioombllem2a  23344  uniioombllem2  23345  uniioombllem3a  23346  uniioombllem3  23347  uniioombllem4  23348  uniioombllem6  23350  dyadmaxlem  23359  volivth  23369  vitalilem2  23372  vitalilem5  23375  i1frn  23438  itg2monolem1  23511  itgcnlem  23550  itgrevallem1  23555  itgreval  23557  itgle  23570  ibladd  23581  iblabslem  23588  itgspliticc  23597  itgsplitioo  23598  ditgcl  23616  ditgswap  23617  ditgsplitlem  23618  limcdif  23634  limcresi  23643  limccnp  23649  limccnp2  23650  limcco  23651  dvlip  23750  dvlip2  23752  dveq0  23757  dvgt0lem1  23759  dvivthlem1  23765  dvcnvrelem1  23774  dvcnvre  23776  dvfsumlem2  23784  ftc1lem1  23792  ftc1a  23794  ftc1lem4  23796  ftc2ditglem  23802  itgsubstlem  23805  ply1rem  23917  fta1glem1  23919  ig1pdvds  23930  plyrem  24054  facth  24055  fta1lem  24056  vieta1lem1  24059  vieta1lem2  24060  aaliou3lem3  24093  aaliou3lem4  24095  aaliou3lem7  24098  taylfvallem1  24105  tayl0  24110  taylply2  24116  radcnvle  24168  psercnlem2  24172  psercnlem1  24173  psercn  24174  pserdvlem1  24175  pserdvlem2  24176  abelth2  24190  coseq00topi  24248  coseq0negpitopi  24249  cosordlem  24271  tanord1  24277  efif1olem1  24282  loglesqrt  24493  logreclem  24494  relogbval  24504  nnlogbexp  24513  chordthmlem4  24556  quart1  24577  quartlem2  24579  quartlem3  24580  quartlem4  24581  quart  24582  acosbnd  24621  atancj  24631  atanlogsublem  24636  atantan  24644  atanbndlem  24646  dvatan  24656  atantayl  24658  rlimcnp2  24687  divsqrtsumlem  24700  ftalem5  24797  ftalem7  24799  basellem4  24804  basellem5  24805  perfectlem2  24949  dchrinv  24980  chpdifbndlem1  25236  pntibndlem2  25274  pntlemc  25278  pntlema  25279  pntlemb  25280  pntlemg  25281  pntlemh  25282  pntlemq  25284  pntlemr  25285  pntlemj  25286  pntlemi  25287  pntlemf  25288  pntlemk  25289  pntlemo  25290  pntleme  25291  pntlem3  25292  pntleml  25294  abvcxp  25298  axtgpasch  25360  cgr3simp2  25410  legso  25488  hlne2  25495  hlln  25496  mirhl  25568  hlperpnel  25611  opphllem4  25636  inagswap  25724  subumgredg2  26171  upgrres1  26199  nb3grprlem1  26276  wlkp  26506  wspthsswwlkn  26808  2wlkdlem6  26821  clwwlknbp0  26878  clwwisshclwwsn  26922  erclwwlkseqlen  26926  erclwwlkssym  26928  erclwwlkstr  26929  extwwlkfablem1  27195  grpoass  27341  vcsm  27401  nvf  27499  ssps  27569  minvecolem2  27715  minvecolem4c  27719  minvecolem4  27720  minvecolem5  27721  minvecolem6  27722  eigvec1  28805  eliccelico  29524  elicoelioo  29525  slmdvsdi  29753  slmdvs1  29758  pmtrto1cl  29834  cnre2csqlem  29941  lmxrge0  29983  sigaclci  30180  difelsiga  30181  insiga  30185  ldsysgenld  30208  sigapildsyslem  30209  sigapildsys  30210  ldgenpisyslem1  30211  measvnul  30254  sibfrn  30384  eulerpartlemt  30418  eulerpartlemmf  30422  tg5segofs  30736  subfacp1lem2a  31147  subfacp1lem3  31149  subfacp1lem4  31150  subfacp1lem5  31151  sconnpht2  31205  sconnpi1  31206  resconn  31213  cvmsss  31234  cvmsn0  31235  cvmlift2lem3  31272  cvmlift2lem7  31276  cvmliftphtlem  31284  cvmliftpht  31285  cvmlift3lem5  31290  cvmlift3lem6  31291  msrf  31424  elmsta  31430  mclsax  31451  mthmpps  31464  mclspps  31466  scutun12  31901  slerec  31907  ivthALT  32314  poimirlem17  33406  poimirlem20  33409  ibladdnc  33447  iblabsnclem  33453  ftc1cnnclem  33463  ftc1anc  33473  ftc2nc  33474  heiborlem3  33592  iccbnd  33619  rngohom1  33747  idl0cl  33797  maxidlnr  33821  lshpne  34095  opococ  34308  opexmid  34320  hlclat  34471  lclkrslem2  36653  gneispacern2  38263  cvgdvgrat  38338  iccshift  39553  iccsuble  39554  icoiccdif  39559  mullimc  39654  limccog  39658  mullimcf  39661  lptioo2  39669  limcmptdm  39673  limcicciooub  39675  icccncfext  39869  cncfioobdlem  39878  ditgeqiooicc  39945  itgsubsticc  39961  iblcncfioo  39963  itgiccshift  39965  itgperiod  39966  itgsbtaddcnst  39967  stoweidlem11  39997  stoweidlem31  40017  stoweidlem36  40022  stoweidlem38  40024  stoweidlem44  40030  stoweidlem62  40048  dirkercncflem1  40089  dirkercncflem4  40092  fourierdlem26  40119  fourierdlem32  40125  fourierdlem33  40126  fourierdlem37  40130  fourierdlem42  40135  fourierdlem54  40146  fourierdlem63  40155  fourierdlem64  40156  fourierdlem65  40157  fourierdlem69  40161  fourierdlem74  40166  fourierdlem75  40167  fourierdlem79  40171  fourierdlem81  40173  fourierdlem82  40174  fourierdlem89  40181  fourierdlem90  40182  fourierdlem91  40183  fourierdlem93  40185  fourierdlem101  40193  fourierdlem111  40203  saldifcl  40308  unisalgen2  40341  hoidmv1lelem3  40576  smff  40710  smfpimltxr  40725  sigardiv  40819  sigarcol  40822  sharhght  40823  sigaradd  40824  cevathlem1  40825  cevathlem2  40826  cevath  40827  proththd  41302  perfectALTVlem2  41402
  Copyright terms: Public domain W3C validator