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

Theorem simp2d 1066
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 1054 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  simp2bi  1069  f1dom3fv3dif  6398  f1dom3el3dif  6399  f1prex  6412  oeeui  7541  erinxp  7680  resixp  7801  domssex  7978  cantnflem1a  8437  cantnflem1d  8440  cantnflem3  8443  cantnflem4  8444  fpwwe2lem7  9309  canthnumlem  9321  canthp1lem2  9326  wun0  9391  lelttrdi  10045  supmullem2  10836  supmul  10837  ixxdisj  12012  ixxun  12013  ixxss1  12015  ixxss2  12016  ixxss12  12017  ixxub  12018  ixxlb  12019  ubioo  12029  elicore  12048  iccgelb  12052  iccss2  12066  icodisj  12119  xov1plusxeqvd  12140  fldiv  12471  immul  13665  sqrtge0  13787  sqrtrege0  13894  icco1  14060  ruclem2  14741  ruclem3  14742  ruclem8  14746  ruclem12  14750  gcddvds  15004  crth  15262  phimullem  15263  eulerthlem1  15265  eulerthlem2  15266  prmreclem3  15401  sectcan  16179  sectco  16180  sectmon  16206  monsect  16207  funcixp  16291  funcsect  16296  invfuc  16398  coapm  16485  catciso  16521  posasymb  16716  ipodrsima  16929  pstr2  16969  psdmrn  16971  psref  16972  mhmlin  17106  subm0cl  17116  eqger  17408  eqgcpbl  17412  gaorber  17505  orbstafun  17508  cayleyth  17599  pmtrrn2  17644  pmtrfinv  17645  dfod2  17745  sylow2blem1  17799  dprdf  18169  dprdff  18175  dprdfcl  18176  dprdsplit  18211  dpjcntz  18215  ablfac1a  18232  ablfac1b  18233  lmodvsdi  18650  lbssp  18841  2idlcpbl  18996  assaring  19082  mpff  19295  mpfaddcl  19296  mpfmulcl  19297  mpfind  19298  pf1rcl  19475  mpfpf1  19477  mdetunilem2  20175  mdetunilem5  20178  mdetunilem6  20179  chfacfisfcpmat  20416  pnfnei  20771  cnptop2  20794  lmcl  20848  lmcnp  20855  flimfil  21520  tlmlmod  21739  ustbasel  21757  ustincl  21758  ustinvel  21760  ustfilxp  21763  tusunif  21820  imasdsf1olem  21924  xmeter  21984  tmsds  22035  metustexhalf  22107  nlmlmod  22220  qdensere  22310  blcvx  22336  tgqioo  22338  icccmplem2  22361  reconnlem1  22364  cnmpt2pc  22461  phtpcer  22528  phtpcerOLD  22529  phtpcco2  22533  pcohtpylem  22553  pcohtpy  22554  pcophtb  22563  om1addcl  22567  pi1blem  22573  pi1cpbl  22578  pi1grplem  22583  pi1inv  22586  pi1xfrf  22587  pi1xfr  22589  pi1xfrcnvlem  22590  pi1cof  22593  pi1coghm  22595  cphnlm  22699  cphsqrtcl2  22713  tchcph  22760  lmcau  22831  bcthlem4  22844  minveclem4c  22916  minveclem2  22917  minveclem3b  22919  minveclem4  22923  minveclem6  22925  ivthicc  22946  ovolfsval  22958  ovollb2lem  22975  ovolshftlem1  22996  ovolscalem1  23000  ovolicc1  23003  ovolicc2lem2  23005  ovolicc2lem4  23007  ovolicc2lem5  23008  ovolicopnf  23011  ioombl1lem1  23045  ioombl1lem3  23047  ioombl1lem4  23048  uniioovol  23065  uniioombllem2a  23068  uniioombllem2  23069  uniioombllem3a  23070  uniioombllem3  23071  uniioombllem4  23072  uniioombllem6  23074  dyadmaxlem  23083  volivth  23093  vitalilem2  23096  vitalilem5  23099  i1frn  23162  itg2monolem1  23235  itgcnlem  23274  itgrevallem1  23279  itgreval  23281  itgle  23294  ibladd  23305  iblabslem  23312  itgspliticc  23321  itgsplitioo  23322  ditgcl  23340  ditgswap  23341  ditgsplitlem  23342  limcdif  23358  limcresi  23367  limccnp  23373  limccnp2  23374  limcco  23375  dvlip  23472  dvlip2  23474  dveq0  23479  dvgt0lem1  23481  dvivthlem1  23487  dvcnvrelem1  23496  dvcnvre  23498  dvfsumlem2  23506  ftc1lem1  23514  ftc1a  23516  ftc1lem4  23518  ftc2ditglem  23524  itgsubstlem  23527  ply1rem  23639  fta1glem1  23641  ig1pdvds  23652  plyrem  23776  facth  23777  fta1lem  23778  vieta1lem1  23781  vieta1lem2  23782  aaliou3lem3  23815  aaliou3lem4  23817  aaliou3lem7  23820  taylfvallem1  23827  tayl0  23832  taylply2  23838  radcnvle  23890  psercnlem2  23894  psercnlem1  23895  psercn  23896  pserdvlem1  23897  pserdvlem2  23898  abelth2  23912  coseq00topi  23970  coseq0negpitopi  23971  cosordlem  23993  tanord1  23999  efif1olem1  24004  loglesqrt  24211  logreclem  24212  relogbval  24222  nnlogbexp  24231  chordthmlem4  24274  quart1  24295  quartlem2  24297  quartlem3  24298  quartlem4  24299  quart  24300  acosbnd  24339  atancj  24349  atanlogsublem  24354  atantan  24362  atanbndlem  24364  dvatan  24374  atantayl  24376  rlimcnp2  24405  divsqrtsumlem  24418  ftalem5  24515  ftalem7  24517  basellem4  24522  basellem5  24523  perfectlem2  24667  dchrinv  24698  chpdifbndlem1  24954  pntibndlem2  24992  pntlemc  24996  pntlema  24997  pntlemb  24998  pntlemg  24999  pntlemh  25000  pntlemq  25002  pntlemr  25003  pntlemj  25004  pntlemi  25005  pntlemf  25006  pntlemk  25007  pntlemo  25008  pntleme  25009  pntlem3  25010  pntleml  25012  abvcxp  25016  axtgpasch  25078  cgr3simp2  25129  legso  25207  hlne2  25214  hlln  25215  mirhl  25287  hlperpnel  25330  opphllem4  25355  inagswap  25443  wlkonwlk  25826  constr3pth  25949  vfwlkniswwlkn  25995  clwwlknscsh  26108  erclwwlknsym  26115  erclwwlkntr  26116  eupaf1o  26258  grpoass  26502  vcsm  26565  nvf  26686  ssps  26768  minvecolem2  26916  minvecolem4c  26920  minvecolem4  26921  minvecolem5  26922  minvecolem6  26923  eigvec1  28006  eliccelico  28730  elicoelioo  28731  slmdvsdi  28900  slmdvs1  28905  pmtrto1cl  28981  cnre2csqlem  29085  lmxrge0  29127  sigaclci  29323  difelsiga  29324  insiga  29328  ldsysgenld  29351  sigapildsyslem  29352  sigapildsys  29353  ldgenpisyslem1  29354  measvnul  29397  sibfrn  29527  eulerpartlemt  29561  eulerpartlemmf  29565  tg5segofs  29805  subfacp1lem2a  30217  subfacp1lem3  30219  subfacp1lem4  30220  subfacp1lem5  30221  sconpht2  30275  sconpi1  30276  rescon  30283  cvmsss  30304  cvmsn0  30305  cvmlift2lem3  30342  cvmlift2lem7  30346  cvmliftphtlem  30354  cvmliftpht  30355  cvmlift3lem5  30360  cvmlift3lem6  30361  msrf  30494  elmsta  30500  mclsax  30521  mthmpps  30534  mclspps  30536  ivthALT  31301  poimirlem17  32394  poimirlem20  32397  ibladdnc  32435  iblabsnclem  32441  ftc1cnnclem  32451  ftc1anc  32461  ftc2nc  32462  heiborlem3  32580  iccbnd  32607  rngohom1  32735  idl0cl  32785  maxidlnr  32809  lshpne  33085  opococ  33298  opexmid  33310  hlclat  33461  lclkrslem2  35643  gneispacern2  37255  cvgdvgrat  37332  iccshift  38390  iccsuble  38391  icoiccdif  38396  mullimc  38482  limccog  38486  mullimcf  38489  lptioo2  38497  limcmptdm  38501  limcicciooub  38503  icccncfext  38572  cncfioobdlem  38581  ditgeqiooicc  38651  itgsubsticc  38667  iblcncfioo  38669  itgiccshift  38671  itgperiod  38672  itgsbtaddcnst  38673  stoweidlem11  38703  stoweidlem31  38723  stoweidlem36  38728  stoweidlem38  38730  stoweidlem44  38736  stoweidlem62  38754  dirkercncflem1  38795  dirkercncflem4  38798  fourierdlem26  38825  fourierdlem32  38831  fourierdlem33  38832  fourierdlem37  38836  fourierdlem42  38841  fourierdlem54  38852  fourierdlem63  38861  fourierdlem64  38862  fourierdlem65  38863  fourierdlem69  38867  fourierdlem74  38872  fourierdlem75  38873  fourierdlem79  38877  fourierdlem81  38879  fourierdlem82  38880  fourierdlem89  38887  fourierdlem90  38888  fourierdlem91  38889  fourierdlem93  38891  fourierdlem101  38899  fourierdlem111  38909  saldifcl  39014  unisalgen2  39047  hoidmv1lelem3  39282  smff  39417  smfpimltxr  39433  sigardiv  39498  sigarcol  39501  sharhght  39502  sigaradd  39503  cevathlem1  39504  cevathlem2  39505  cevath  39506  proththd  39869  perfectALTVlem2  39965  subumgredg2  40506  upgrres1  40529  nb3grprlem1  40605  wspthsswwlkn  41122  21wlkdlem6  41135  clwwlknbp0  41189  clwwisshclwwsn  41233  erclwwlkseqlen  41237  erclwwlkssym  41239  erclwwlkstr  41240  av-extwwlkfablem1  41505
  Copyright terms: Public domain W3C validator