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

Theorem simp2d 1139
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 1133 . 2 ((𝜓𝜒𝜃) → 𝜒)
31, 2syl 17 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1083
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 209  df-an 399  df-3an 1085
This theorem is referenced by:  simp2bi  1142  f1dom3fv3dif  7025  f1dom3el3dif  7026  f1prex  7039  oeeui  8227  resixp  8496  domssex  8677  cantnflem1a  9147  cantnflem1d  9150  cantnflem3  9153  cantnflem4  9154  fpwwe2lem7  10057  canthnumlem  10069  canthp1lem2  10074  wun0  10139  lelttrdi  10801  supmullem2  11611  supmul  11612  ixxdisj  12752  ixxun  12753  ixxss1  12755  ixxss2  12756  ixxss12  12757  ixxub  12758  ixxlb  12759  ubioo  12769  elicore  12788  iccgelb  12792  iccss2  12806  icodisj  12861  xov1plusxeqvd  12883  fldiv  13227  immul  14494  sqrtge0  14616  sqrtrege0  14724  icco1  14896  ruclem2  15584  ruclem3  15585  ruclem8  15589  ruclem12  15593  gcddvds  15851  crth  16114  phimullem  16115  eulerthlem1  16117  eulerthlem2  16118  prmreclem3  16253  sectcan  17024  sectco  17025  sectmon  17051  monsect  17052  funcixp  17136  funcsect  17141  invfuc  17243  coapm  17330  catciso  17366  posasymb  17561  ipodrsima  17774  pstr2  17814  psdmrn  17816  psref  17817  mhmlin  17962  subm0cl  17975  eqger  18329  eqgcpbl  18333  gaorber  18437  orbstafun  18440  cayleyth  18542  pmtrrn2  18587  pmtrfinv  18588  dfod2  18690  sylow2blem1  18744  dprdf  19127  dprdff  19133  dprdfcl  19134  dprdsplit  19169  dpjcntz  19173  ablfac1a  19190  ablfac1b  19191  lmodvsdi  19656  lbssp  19850  2idlcpbl  20006  assaring  20092  mpff  20316  mpfaddcl  20317  mpfmulcl  20318  mpfind  20319  pf1rcl  20511  mpfpf1  20513  mdetunilem2  21221  mdetunilem5  21224  mdetunilem6  21225  chfacfisfcpmat  21462  pnfnei  21827  cnptop2  21850  lmcl  21904  lmcnp  21911  flimfil  22576  tlmlmod  22796  ustbasel  22814  ustincl  22815  ustinvel  22817  ustfilxp  22820  tusunif  22877  imasdsf1olem  22982  xmeter  23042  tmsds  23093  metustexhalf  23165  nlmlmod  23286  qdensere  23377  blcvx  23405  tgqioo  23407  icccmplem2  23430  reconnlem1  23433  cnmpopc  23531  phtpcer  23598  phtpcco2  23602  pcohtpylem  23622  pcohtpy  23623  pcophtb  23632  om1addcl  23636  pi1blem  23642  pi1cpbl  23647  pi1grplem  23652  pi1inv  23655  pi1xfrf  23656  pi1xfr  23658  pi1xfrcnvlem  23659  pi1cof  23662  pi1coghm  23664  cphnlm  23775  cphsqrtcl2  23789  tcphcph  23839  lmcau  23915  bcthlem4  23929  minveclem4c  24027  minveclem2  24028  minveclem3b  24030  minveclem4  24034  minveclem6  24036  ivthicc  24058  ovolfsval  24070  ovollb2lem  24088  ovolshftlem1  24109  ovolscalem1  24113  ovolicc1  24116  ovolicc2lem2  24118  ovolicc2lem4  24120  ovolicc2lem5  24121  ovolicopnf  24124  ioombl1lem1  24158  ioombl1lem3  24160  ioombl1lem4  24161  uniioovol  24179  uniioombllem2a  24182  uniioombllem2  24183  uniioombllem3a  24184  uniioombllem3  24185  uniioombllem4  24186  uniioombllem6  24188  dyadmaxlem  24197  volivth  24207  vitalilem2  24209  vitalilem5  24212  i1frn  24277  itg2monolem1  24350  itgcnlem  24389  itgrevallem1  24394  itgreval  24396  itgle  24409  ibladd  24420  iblabslem  24427  itgspliticc  24436  itgsplitioo  24437  ditgcl  24455  ditgswap  24456  ditgsplitlem  24457  limcdif  24473  limcresi  24482  limccnp  24488  limccnp2  24489  limcco  24490  dvlip  24589  dvlip2  24591  dveq0  24596  dvgt0lem1  24598  dvivthlem1  24604  dvcnvrelem1  24613  dvcnvre  24615  dvfsumlem2  24623  ftc1lem1  24631  ftc1a  24633  ftc1lem4  24635  ftc2ditglem  24641  itgsubstlem  24644  ply1rem  24756  fta1glem1  24758  ig1pdvds  24769  plyrem  24893  facth  24894  fta1lem  24895  vieta1lem1  24898  vieta1lem2  24899  aaliou3lem3  24932  aaliou3lem4  24934  aaliou3lem7  24937  taylfvallem1  24944  tayl0  24949  taylply2  24955  radcnvle  25007  psercnlem2  25011  psercnlem1  25012  psercn  25013  pserdvlem1  25014  pserdvlem2  25015  abelth2  25029  coseq00topi  25087  coseq0negpitopi  25088  cosordlem  25114  tanord1  25120  efif1olem1  25125  loglesqrt  25338  logreclem  25339  relogbval  25349  nnlogbexp  25358  chordthmlem4  25412  quart1  25433  quartlem2  25435  quartlem3  25436  quartlem4  25437  quart  25438  acosbnd  25477  atancj  25487  atanlogsublem  25492  atantan  25500  atanbndlem  25502  dvatan  25512  atantayl  25514  rlimcnp2  25543  divsqrtsumlem  25556  ftalem5  25653  ftalem7  25655  basellem4  25660  basellem5  25661  perfectlem2  25805  dchrinv  25836  chpdifbndlem1  26128  pntibndlem2  26166  pntlemc  26170  pntlema  26171  pntlemb  26172  pntlemg  26173  pntlemh  26174  pntlemq  26176  pntlemr  26177  pntlemj  26178  pntlemi  26179  pntlemf  26180  pntlemk  26181  pntlemo  26182  pntleme  26183  pntlem3  26184  pntleml  26186  abvcxp  26190  axtgpasch  26252  cgr3simp2  26306  legso  26384  hlne2  26391  hlln  26392  mirhl  26464  inagswap  26626  inagne2  26628  dfcgrg2  26648  subumgredg2  27066  upgrres1  27094  nb3grprlem1  27161  wlkp  27397  wspthsswwlkn  27696  2wlkdlem6  27709  clwwisshclwwsn  27793  erclwwlkeqlen  27796  erclwwlksym  27798  erclwwlktr  27799  clwwlkn  27803  clwwlknwrd  27811  clwwlknonex2e  27888  grpoass  28279  vcsm  28338  nvf  28436  ssps  28506  minvecolem2  28651  minvecolem4c  28655  minvecolem4  28656  minvecolem5  28657  minvecolem6  28658  eigvec1  29738  eliccelico  30499  elicoelioo  30500  pmtrto1cl  30741  cyc3evpm  30792  slmdvsdi  30843  slmdvs1  30848  imaslmod  30922  prmidlnr  30956  qsidomlem2  30966  mxidlnr  30973  cnre2csqlem  31153  lmxrge0  31195  sigaclci  31391  difelsiga  31392  insiga  31396  ldsysgenld  31419  sigapildsyslem  31420  sigapildsys  31421  ldgenpisyslem1  31422  measvnul  31465  sibfrn  31595  eulerpartlemt  31629  eulerpartlemmf  31633  tg5segofs  31944  lpadleft  31954  spthcycl  32376  subgrwlk  32379  acycgrcycl  32394  subfacp1lem2a  32427  subfacp1lem3  32429  subfacp1lem4  32430  subfacp1lem5  32431  sconnpht2  32485  sconnpi1  32486  resconn  32493  cvmsss  32514  cvmsn0  32515  cvmlift2lem3  32552  cvmlift2lem7  32556  cvmliftphtlem  32564  cvmliftpht  32565  cvmlift3lem5  32570  cvmlift3lem6  32571  msrf  32789  elmsta  32795  mclsax  32816  mthmpps  32829  mclspps  32831  scutun12  33271  slerec  33277  ivthALT  33683  poimirlem17  34908  poimirlem20  34911  ibladdnc  34948  iblabsnclem  34954  ftc1cnnclem  34964  ftc1anc  34974  ftc2nc  34975  heiborlem3  35090  iccbnd  35117  rngohom1  35245  idl0cl  35295  maxidlnr  35319  lshpne  36117  opococ  36330  opexmid  36342  hlclat  36493  lclkrslem2  38673  gneispacern2  40487  cvgdvgrat  40643  iccshift  41792  iccsuble  41793  icoiccdif  41798  mullimc  41895  limccog  41899  mullimcf  41902  lptioo2  41910  limcmptdm  41914  limcicciooub  41916  xlimmnfvlem1  42111  xlimpnfvlem1  42115  icccncfext  42168  cncfioobdlem  42177  ditgeqiooicc  42243  itgsubsticc  42259  iblcncfioo  42261  itgiccshift  42263  itgperiod  42264  itgsbtaddcnst  42265  stoweidlem11  42295  stoweidlem31  42315  stoweidlem36  42320  stoweidlem38  42322  stoweidlem44  42328  stoweidlem62  42346  dirkercncflem1  42387  dirkercncflem4  42390  fourierdlem26  42417  fourierdlem32  42423  fourierdlem33  42424  fourierdlem37  42428  fourierdlem42  42433  fourierdlem54  42444  fourierdlem63  42453  fourierdlem64  42454  fourierdlem65  42455  fourierdlem69  42459  fourierdlem74  42464  fourierdlem75  42465  fourierdlem79  42469  fourierdlem81  42471  fourierdlem82  42472  fourierdlem89  42479  fourierdlem90  42480  fourierdlem91  42481  fourierdlem93  42483  fourierdlem101  42491  fourierdlem111  42501  saldifcl  42603  unisalgen2  42636  hoidmv1lelem3  42874  smff  43008  smfpimltxr  43023  sigardiv  43117  sigarcol  43120  sharhght  43121  sigaradd  43122  cevathlem1  43123  cevathlem2  43124  cevath  43125  proththd  43778  perfectALTVlem2  43886
  Copyright terms: Public domain W3C validator