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

Theorem simp2d 1067
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 1055 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  simp2bi  1070  f1dom3fv3dif  6425  f1dom3el3dif  6426  f1prex  6439  oeeui  7569  erinxp  7708  resixp  7829  domssex  8006  cantnflem1a  8465  cantnflem1d  8468  cantnflem3  8471  cantnflem4  8472  fpwwe2lem7  9337  canthnumlem  9349  canthp1lem2  9354  wun0  9419  lelttrdi  10078  supmullem2  10871  supmul  10872  ixxdisj  12061  ixxun  12062  ixxss1  12064  ixxss2  12065  ixxss12  12066  ixxub  12067  ixxlb  12068  ubioo  12078  elicore  12097  iccgelb  12101  iccss2  12115  icodisj  12168  xov1plusxeqvd  12189  fldiv  12521  immul  13724  sqrtge0  13846  sqrtrege0  13953  icco1  14119  ruclem2  14800  ruclem3  14801  ruclem8  14805  ruclem12  14809  gcddvds  15063  crth  15321  phimullem  15322  eulerthlem1  15324  eulerthlem2  15325  prmreclem3  15460  sectcan  16238  sectco  16239  sectmon  16265  monsect  16266  funcixp  16350  funcsect  16355  invfuc  16457  coapm  16544  catciso  16580  posasymb  16775  ipodrsima  16988  pstr2  17028  psdmrn  17030  psref  17031  mhmlin  17165  subm0cl  17175  eqger  17467  eqgcpbl  17471  gaorber  17564  orbstafun  17567  cayleyth  17658  pmtrrn2  17703  pmtrfinv  17704  dfod2  17804  sylow2blem1  17858  dprdf  18228  dprdff  18234  dprdfcl  18235  dprdsplit  18270  dpjcntz  18274  ablfac1a  18291  ablfac1b  18292  lmodvsdi  18709  lbssp  18900  2idlcpbl  19055  assaring  19141  mpff  19354  mpfaddcl  19355  mpfmulcl  19356  mpfind  19357  pf1rcl  19534  mpfpf1  19536  mdetunilem2  20238  mdetunilem5  20241  mdetunilem6  20242  chfacfisfcpmat  20479  pnfnei  20834  cnptop2  20857  lmcl  20911  lmcnp  20918  flimfil  21583  tlmlmod  21802  ustbasel  21820  ustincl  21821  ustinvel  21823  ustfilxp  21826  tusunif  21883  imasdsf1olem  21988  xmeter  22048  tmsds  22099  metustexhalf  22171  nlmlmod  22292  qdensere  22383  blcvx  22409  tgqioo  22411  icccmplem2  22434  reconnlem1  22437  cnmpt2pc  22535  phtpcer  22602  phtpcerOLD  22603  phtpcco2  22607  pcohtpylem  22627  pcohtpy  22628  pcophtb  22637  om1addcl  22641  pi1blem  22647  pi1cpbl  22652  pi1grplem  22657  pi1inv  22660  pi1xfrf  22661  pi1xfr  22663  pi1xfrcnvlem  22664  pi1cof  22667  pi1coghm  22669  cphnlm  22780  cphsqrtcl2  22794  tchcph  22844  lmcau  22919  bcthlem4  22932  minveclem4c  23004  minveclem2  23005  minveclem3b  23007  minveclem4  23011  minveclem6  23013  ivthicc  23034  ovolfsval  23046  ovollb2lem  23063  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ovolicc2lem2  23093  ovolicc2lem4  23095  ovolicc2lem5  23096  ovolicopnf  23099  ioombl1lem1  23133  ioombl1lem3  23135  ioombl1lem4  23136  uniioovol  23153  uniioombllem2a  23156  uniioombllem2  23157  uniioombllem3a  23158  uniioombllem3  23159  uniioombllem4  23160  uniioombllem6  23162  dyadmaxlem  23171  volivth  23181  vitalilem2  23184  vitalilem5  23187  i1frn  23250  itg2monolem1  23323  itgcnlem  23362  itgrevallem1  23367  itgreval  23369  itgle  23382  ibladd  23393  iblabslem  23400  itgspliticc  23409  itgsplitioo  23410  ditgcl  23428  ditgswap  23429  ditgsplitlem  23430  limcdif  23446  limcresi  23455  limccnp  23461  limccnp2  23462  limcco  23463  dvlip  23560  dvlip2  23562  dveq0  23567  dvgt0lem1  23569  dvivthlem1  23575  dvcnvrelem1  23584  dvcnvre  23586  dvfsumlem2  23594  ftc1lem1  23602  ftc1a  23604  ftc1lem4  23606  ftc2ditglem  23612  itgsubstlem  23615  ply1rem  23727  fta1glem1  23729  ig1pdvds  23740  plyrem  23864  facth  23865  fta1lem  23866  vieta1lem1  23869  vieta1lem2  23870  aaliou3lem3  23903  aaliou3lem4  23905  aaliou3lem7  23908  taylfvallem1  23915  tayl0  23920  taylply2  23926  radcnvle  23978  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  abelth2  24000  coseq00topi  24058  coseq0negpitopi  24059  cosordlem  24081  tanord1  24087  efif1olem1  24092  loglesqrt  24299  logreclem  24300  relogbval  24310  nnlogbexp  24319  chordthmlem4  24362  quart1  24383  quartlem2  24385  quartlem3  24386  quartlem4  24387  quart  24388  acosbnd  24427  atancj  24437  atanlogsublem  24442  atantan  24450  atanbndlem  24452  dvatan  24462  atantayl  24464  rlimcnp2  24493  divsqrtsumlem  24506  ftalem5  24603  ftalem7  24605  basellem4  24610  basellem5  24611  perfectlem2  24755  dchrinv  24786  chpdifbndlem1  25042  pntibndlem2  25080  pntlemc  25084  pntlema  25085  pntlemb  25086  pntlemg  25087  pntlemh  25088  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemi  25093  pntlemf  25094  pntlemk  25095  pntlemo  25096  pntleme  25097  pntlem3  25098  pntleml  25100  abvcxp  25104  axtgpasch  25166  cgr3simp2  25216  legso  25294  hlne2  25301  hlln  25302  mirhl  25374  hlperpnel  25417  opphllem4  25442  inagswap  25530  wlkonwlk  26065  constr3pth  26188  vfwlkniswwlkn  26234  clwwlknscsh  26347  erclwwlknsym  26354  erclwwlkntr  26355  eupaf1o  26497  grpoass  26741  vcsm  26801  nvf  26899  ssps  26969  minvecolem2  27115  minvecolem4c  27119  minvecolem4  27120  minvecolem5  27121  minvecolem6  27122  eigvec1  28205  eliccelico  28929  elicoelioo  28930  slmdvsdi  29099  slmdvs1  29104  pmtrto1cl  29180  cnre2csqlem  29284  lmxrge0  29326  sigaclci  29522  difelsiga  29523  insiga  29527  ldsysgenld  29550  sigapildsyslem  29551  sigapildsys  29552  ldgenpisyslem1  29553  measvnul  29596  sibfrn  29726  eulerpartlemt  29760  eulerpartlemmf  29764  tg5segofs  30004  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem4  30419  subfacp1lem5  30420  sconpht2  30474  sconpi1  30475  rescon  30482  cvmsss  30503  cvmsn0  30504  cvmlift2lem3  30541  cvmlift2lem7  30545  cvmliftphtlem  30553  cvmliftpht  30554  cvmlift3lem5  30559  cvmlift3lem6  30560  msrf  30693  elmsta  30699  mclsax  30720  mthmpps  30733  mclspps  30735  ivthALT  31500  poimirlem17  32596  poimirlem20  32599  ibladdnc  32637  iblabsnclem  32643  ftc1cnnclem  32653  ftc1anc  32663  ftc2nc  32664  heiborlem3  32782  iccbnd  32809  rngohom1  32937  idl0cl  32987  maxidlnr  33011  lshpne  33287  opococ  33500  opexmid  33512  hlclat  33663  lclkrslem2  35845  gneispacern2  37457  cvgdvgrat  37534  iccshift  38591  iccsuble  38592  icoiccdif  38597  mullimc  38683  limccog  38687  mullimcf  38690  lptioo2  38698  limcmptdm  38702  limcicciooub  38704  icccncfext  38773  cncfioobdlem  38782  ditgeqiooicc  38852  itgsubsticc  38868  iblcncfioo  38870  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem11  38904  stoweidlem31  38924  stoweidlem36  38929  stoweidlem38  38931  stoweidlem44  38937  stoweidlem62  38955  dirkercncflem1  38996  dirkercncflem4  38999  fourierdlem26  39026  fourierdlem32  39032  fourierdlem33  39033  fourierdlem37  39037  fourierdlem42  39042  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem69  39068  fourierdlem74  39073  fourierdlem75  39074  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem93  39092  fourierdlem101  39100  fourierdlem111  39110  saldifcl  39215  unisalgen2  39248  hoidmv1lelem3  39483  smff  39618  smfpimltxr  39634  sigardiv  39699  sigarcol  39702  sharhght  39703  sigaradd  39704  cevathlem1  39705  cevathlem2  39706  cevath  39707  proththd  40069  perfectALTVlem2  40165  subumgredg2  40509  upgrres1  40532  nb3grprlem1  40608  wspthsswwlkn  41125  21wlkdlem6  41138  clwwlknbp0  41192  clwwisshclwwsn  41236  erclwwlkseqlen  41240  erclwwlkssym  41242  erclwwlkstr  41243  av-extwwlkfablem1  41508
  Copyright terms: Public domain W3C validator