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

Theorem simp2d 1135
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 1129 . 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:  simp2bi  1138  f1dom3fv3dif  7017  f1dom3el3dif  7018  f1prex  7031  oeeui  8218  resixp  8486  domssex  8667  cantnflem1a  9137  cantnflem1d  9140  cantnflem3  9143  cantnflem4  9144  fpwwe2lem7  10047  canthnumlem  10059  canthp1lem2  10064  wun0  10129  lelttrdi  10791  supmullem2  11601  supmul  11602  ixxdisj  12743  ixxun  12744  ixxss1  12746  ixxss2  12747  ixxss12  12748  ixxub  12749  ixxlb  12750  ubioo  12760  elicore  12779  iccgelb  12783  iccss2  12797  icodisj  12852  xov1plusxeqvd  12874  fldiv  13218  immul  14485  sqrtge0  14607  sqrtrege0  14715  icco1  14887  ruclem2  15575  ruclem3  15576  ruclem8  15580  ruclem12  15584  gcddvds  15842  crth  16105  phimullem  16106  eulerthlem1  16108  eulerthlem2  16109  prmreclem3  16244  sectcan  17015  sectco  17016  sectmon  17042  monsect  17043  funcixp  17127  funcsect  17132  invfuc  17234  coapm  17321  catciso  17357  posasymb  17552  ipodrsima  17765  pstr2  17805  psdmrn  17807  psref  17808  mhmlin  17953  subm0cl  17966  eqger  18270  eqgcpbl  18274  gaorber  18378  orbstafun  18381  cayleyth  18474  pmtrrn2  18519  pmtrfinv  18520  dfod2  18622  sylow2blem1  18676  dprdf  19059  dprdff  19065  dprdfcl  19066  dprdsplit  19101  dpjcntz  19105  ablfac1a  19122  ablfac1b  19123  lmodvsdi  19588  lbssp  19782  2idlcpbl  19937  assaring  20023  mpff  20247  mpfaddcl  20248  mpfmulcl  20249  mpfind  20250  pf1rcl  20442  mpfpf1  20444  mdetunilem2  21152  mdetunilem5  21155  mdetunilem6  21156  chfacfisfcpmat  21393  pnfnei  21758  cnptop2  21781  lmcl  21835  lmcnp  21842  flimfil  22507  tlmlmod  22726  ustbasel  22744  ustincl  22745  ustinvel  22747  ustfilxp  22750  tusunif  22807  imasdsf1olem  22912  xmeter  22972  tmsds  23023  metustexhalf  23095  nlmlmod  23216  qdensere  23307  blcvx  23335  tgqioo  23337  icccmplem2  23360  reconnlem1  23363  cnmpopc  23461  phtpcer  23528  phtpcco2  23532  pcohtpylem  23552  pcohtpy  23553  pcophtb  23562  om1addcl  23566  pi1blem  23572  pi1cpbl  23577  pi1grplem  23582  pi1inv  23585  pi1xfrf  23586  pi1xfr  23588  pi1xfrcnvlem  23589  pi1cof  23592  pi1coghm  23594  cphnlm  23705  cphsqrtcl2  23719  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  ovolicc1  24046  ovolicc2lem2  24048  ovolicc2lem4  24050  ovolicc2lem5  24051  ovolicopnf  24054  ioombl1lem1  24088  ioombl1lem3  24090  ioombl1lem4  24091  uniioovol  24109  uniioombllem2a  24112  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem6  24118  dyadmaxlem  24127  volivth  24137  vitalilem2  24139  vitalilem5  24142  i1frn  24207  itg2monolem1  24280  itgcnlem  24319  itgrevallem1  24324  itgreval  24326  itgle  24339  ibladd  24350  iblabslem  24357  itgspliticc  24366  itgsplitioo  24367  ditgcl  24385  ditgswap  24386  ditgsplitlem  24387  limcdif  24403  limcresi  24412  limccnp  24418  limccnp2  24419  limcco  24420  dvlip  24519  dvlip2  24521  dveq0  24526  dvgt0lem1  24528  dvivthlem1  24534  dvcnvrelem1  24543  dvcnvre  24545  dvfsumlem2  24553  ftc1lem1  24561  ftc1a  24563  ftc1lem4  24565  ftc2ditglem  24571  itgsubstlem  24574  ply1rem  24686  fta1glem1  24688  ig1pdvds  24699  plyrem  24823  facth  24824  fta1lem  24825  vieta1lem1  24828  vieta1lem2  24829  aaliou3lem3  24862  aaliou3lem4  24864  aaliou3lem7  24867  taylfvallem1  24874  tayl0  24879  taylply2  24885  radcnvle  24937  psercnlem2  24941  psercnlem1  24942  psercn  24943  pserdvlem1  24944  pserdvlem2  24945  abelth2  24959  coseq00topi  25017  coseq0negpitopi  25018  cosordlem  25042  tanord1  25048  efif1olem1  25053  loglesqrt  25266  logreclem  25267  relogbval  25277  nnlogbexp  25286  chordthmlem4  25340  quart1  25361  quartlem2  25363  quartlem3  25364  quartlem4  25365  quart  25366  acosbnd  25405  atancj  25415  atanlogsublem  25420  atantan  25428  atanbndlem  25430  dvatan  25440  atantayl  25442  rlimcnp2  25472  divsqrtsumlem  25485  ftalem5  25582  ftalem7  25584  basellem4  25589  basellem5  25590  perfectlem2  25734  dchrinv  25765  chpdifbndlem1  26057  pntibndlem2  26095  pntlemc  26099  pntlema  26100  pntlemb  26101  pntlemg  26102  pntlemh  26103  pntlemq  26105  pntlemr  26106  pntlemj  26107  pntlemi  26108  pntlemf  26109  pntlemk  26110  pntlemo  26111  pntleme  26112  pntlem3  26113  pntleml  26115  abvcxp  26119  axtgpasch  26181  cgr3simp2  26235  legso  26313  hlne2  26320  hlln  26321  mirhl  26393  inagswap  26555  inagne2  26557  dfcgrg2  26577  subumgredg2  26995  upgrres1  27023  nb3grprlem1  27090  wlkp  27326  wspthsswwlkn  27625  2wlkdlem6  27638  clwwisshclwwsn  27722  erclwwlkeqlen  27725  erclwwlksym  27727  erclwwlktr  27728  clwwlkn  27732  clwwlknwrd  27740  clwwlknonex2e  27817  grpoass  28208  vcsm  28267  nvf  28365  ssps  28435  minvecolem2  28580  minvecolem4c  28584  minvecolem4  28585  minvecolem5  28586  minvecolem6  28587  eigvec1  29667  eliccelico  30427  elicoelioo  30428  pmtrto1cl  30669  cyc3evpm  30720  slmdvsdi  30771  slmdvs1  30776  imaslmod  30850  prmidlnr  30876  qsidomlem2  30884  cnre2csqlem  31053  lmxrge0  31095  sigaclci  31291  difelsiga  31292  insiga  31296  ldsysgenld  31319  sigapildsyslem  31320  sigapildsys  31321  ldgenpisyslem1  31322  measvnul  31365  sibfrn  31495  eulerpartlemt  31529  eulerpartlemmf  31533  tg5segofs  31844  lpadleft  31854  spthcycl  32274  subgrwlk  32277  acycgrcycl  32292  subfacp1lem2a  32325  subfacp1lem3  32327  subfacp1lem4  32328  subfacp1lem5  32329  sconnpht2  32383  sconnpi1  32384  resconn  32391  cvmsss  32412  cvmsn0  32413  cvmlift2lem3  32450  cvmlift2lem7  32454  cvmliftphtlem  32462  cvmliftpht  32463  cvmlift3lem5  32468  cvmlift3lem6  32469  msrf  32687  elmsta  32693  mclsax  32714  mthmpps  32727  mclspps  32729  scutun12  33169  slerec  33175  ivthALT  33581  poimirlem17  34791  poimirlem20  34794  ibladdnc  34831  iblabsnclem  34837  ftc1cnnclem  34847  ftc1anc  34857  ftc2nc  34858  heiborlem3  34974  iccbnd  35001  rngohom1  35129  idl0cl  35179  maxidlnr  35203  lshpne  36000  opococ  36213  opexmid  36225  hlclat  36376  lclkrslem2  38556  gneispacern2  40369  cvgdvgrat  40525  iccshift  41674  iccsuble  41675  icoiccdif  41680  mullimc  41777  limccog  41781  mullimcf  41784  lptioo2  41792  limcmptdm  41796  limcicciooub  41798  xlimmnfvlem1  41993  xlimpnfvlem1  41997  icccncfext  42050  cncfioobdlem  42059  ditgeqiooicc  42125  itgsubsticc  42141  iblcncfioo  42143  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem11  42177  stoweidlem31  42197  stoweidlem36  42202  stoweidlem38  42204  stoweidlem44  42210  stoweidlem62  42228  dirkercncflem1  42269  dirkercncflem4  42272  fourierdlem26  42299  fourierdlem32  42305  fourierdlem33  42306  fourierdlem37  42310  fourierdlem42  42315  fourierdlem54  42326  fourierdlem63  42335  fourierdlem64  42336  fourierdlem65  42337  fourierdlem69  42341  fourierdlem74  42346  fourierdlem75  42347  fourierdlem79  42351  fourierdlem81  42353  fourierdlem82  42354  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem93  42365  fourierdlem101  42373  fourierdlem111  42383  saldifcl  42485  unisalgen2  42518  hoidmv1lelem3  42756  smff  42890  smfpimltxr  42905  sigardiv  42999  sigarcol  43002  sharhght  43003  sigaradd  43004  cevathlem1  43005  cevathlem2  43006  cevath  43007  proththd  43626  perfectALTVlem2  43734
  Copyright terms: Public domain W3C validator