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

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

Proof of Theorem simp1d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp1 1128 . 2 ((𝜓𝜒𝜃) → 𝜓)
31, 2syl 17 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072
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 385  df-3an 1074
This theorem is referenced by:  simp1bi  1137  f1dom3fv3dif  6676  f1dom3el3dif  6677  f1prex  6690  oeeui  7839  oeeu  7840  erinxp  7976  domssex2  8273  domssex  8274  cantnflem1a  8743  cantnflem1b  8744  cantnflem1c  8745  cantnflem1d  8746  cantnflem1  8747  cantnflem3  8749  cantnflem4  8750  fpwwe2lem7  9621  canthnumlem  9633  canthp1lem2  9638  wuntr  9690  lelttrdi  10362  supmul1  11155  supmullem1  11156  supmullem2  11157  supmul  11158  ixxdisj  12354  ixxun  12355  ixxss1  12357  ixxss2  12358  ixxss12  12359  ixxub  12360  ixxlb  12361  iccss2  12408  iocssre  12417  icossre  12418  iccssre  12419  icodisj  12461  iccf1o  12480  xov1plusxeqvd  12482  fzen  12522  intfracq  12823  fldiv  12824  remul  14039  sqrlem6  14158  resqrtth  14166  sqrtth  14274  ruclem6  15134  ruclem9  15137  ruclem12  15140  gcdn0cl  15397  crth  15656  phimullem  15657  eulerthlem1  15659  eulerthlem2  15660  pcpremul  15721  prmreclem3  15795  sectcan  16587  sectco  16588  sectmon  16614  monsect  16615  funcf1  16698  funcsect  16704  invfuc  16806  coapm  16893  catciso  16929  psrel  17375  pstr  17383  mhmf  17512  submss  17522  eqger  17816  eqgcpbl  17820  gaorber  17912  orbstafun  17915  cayleyth  18006  dprdgrp  18575  dprdff  18582  ablfac1a  18639  ablfac1b  18640  lmodvscl  19053  lbsss  19250  2idlcpbl  19407  assalmod  19492  mpfind  19709  mdetunilem2  20592  mdetunilem5  20595  mdetunilem6  20596  chfacfisfcpmat  20833  cnptop1  21219  lmfpm  21272  lmff  21278  lmcnp  21281  flimtop  21941  tlmtmd  22162  ustssxp  22180  ustdiag  22184  ustfilxp  22188  ustbas2  22201  tusbas  22244  imasdsf1olem  22350  xmeter  22410  tmsbas  22460  metustexhalf  22533  nlmngp  22653  qdensere  22745  blcvx  22773  tgqioo  22775  icccmplem2  22798  reconnlem1  22801  cnmpt2pc  22899  icoopnst  22910  iocopnst  22911  iccpnfcnv  22915  phtpcer  22966  phtpcco2  22970  pcohtpylem  22990  pcohtpy  22991  pcopt  22993  pcopt2  22994  pcorevlem  22997  pcorev2  22999  pcophtb  23000  om1addcl  23004  pi1cpbl  23015  pi1grplem  23020  pi1inv  23023  pi1xfrf  23024  pi1xfr  23026  pi1xfrcnvlem  23027  pi1xfrcnv  23028  pi1cof  23030  pi1coghm  23032  cphphl  23142  cphreccllem  23149  cphsqrtcl2  23157  tchclm  23202  tchcph  23207  lmcau  23282  bcthlem4  23295  minveclem4c  23367  minveclem2  23368  minveclem3b  23370  minveclem4  23374  minveclem6  23376  ivthicc  23398  ovolfsval  23410  ovollb2lem  23427  ovolshftlem1  23448  ovolscalem1  23452  ovolicc2lem2  23457  ovolicc2lem5  23460  ovolicopnf  23463  ioombl1lem1  23497  ioombl1lem3  23499  ioombl1lem4  23500  uniioovol  23518  uniioombllem2a  23521  uniioombllem2  23522  uniioombllem3a  23523  uniioombllem3  23524  uniioombllem4  23525  uniioombllem6  23527  vitalilem2  23548  vitalilem3  23549  vitalilem4  23550  i1ff  23613  itg2monolem1  23687  itgreval  23733  ibladd  23757  iblabslem  23764  itgspliticc  23773  itgsplitioo  23774  ditgcl  23792  ditgswap  23793  ditgsplitlem  23794  ditgsplit  23795  limcresi  23819  dvlip2  23928  dveq0  23933  dvcnvre  23952  dvfsumlem2  23960  ftc1a  23970  ply1rem  24093  facth1  24094  fta1glem1  24095  fta1glem2  24096  ig1pcl  24105  ig1pdvds  24106  plyrem  24230  facth  24231  vieta1lem1  24235  vieta1lem2  24236  aaliou3lem3  24269  aaliou3lem7  24274  pserulm  24346  psercnlem2  24348  psercn  24350  pserdvlem1  24351  pserdvlem2  24352  pserdv  24353  abelth2  24366  coseq00topi  24424  coseq0negpitopi  24425  cosordlem  24447  efif1olem1  24458  dvloglem  24564  loglesqrt  24669  relogbval  24680  nnlogbexp  24689  logbrec  24690  quart1  24753  quartlem2  24755  quartlem3  24756  quartlem4  24757  quart  24758  asinsinlem  24788  atanlogsublem  24812  atans2  24828  dvatan  24832  rlimcnp2  24863  divsqrtsumlem  24876  ftalem5  24973  ftalem7  24975  basellem4  24980  basellem5  24981  perfectlem2  25125  dchrinv  25156  chpdifbndlem1  25412  pntibndlem2  25450  pntlema  25455  pntlemb  25456  pntlemg  25457  pntlemh  25458  pntlemn  25459  pntlemq  25460  pntlemr  25461  pntlemj  25462  pntlemf  25464  pntlemk  25465  pntlemo  25466  pntlemp  25469  pntleml  25470  abvcxp  25474  axtgbtwnid  25535  cgr3simp1  25585  hlne1  25670  hltr  25675  btwnhl  25679  mirhl  25744  opphllem4  25812  hlpasch  25818  inagswap  25900  wlkf  26691  wlk1ewlk  26717  2wlkdlem6  27022  2wlkond  27028  2trlond  27030  grpofo  27633  vcablo  27704  nvvc  27750  sspba  27862  sspg  27863  minvecolem2  28011  minvecolem4c  28015  minvecolem4  28016  minvecolem5  28017  minvecolem6  28018  eleigveccl  29098  xrofsup  29813  eliccelico  29819  elicoelioo  29820  slmdvscl  30047  slmdvsass  30050  baselsiga  30458  insiga  30480  ldsysgenld  30503  sigapildsys  30505  ldgenpisyslem1  30506  measfrge0  30546  sibfmbl  30677  eulerpartlemt  30713  eulerpartlemmf  30717  probfinmeasbOLD  30770  tg5segofs  31031  subfacp1lem2a  31440  subfacp1lem2b  31441  subfacp1lem3  31442  subfacp1lem4  31443  subfacp1lem5  31444  sconnpht2  31498  sconnpi1  31499  cvxsconn  31503  cvmlift2lem3  31565  cvmlift2lem5  31567  cvmlift2lem6  31568  cvmlift2lem7  31569  cvmlift2lem12  31574  cvmliftphtlem  31577  cvmliftpht  31578  cvmlift3lem2  31580  cvmlift3lem4  31582  cvmlift3lem5  31583  cvmlift3lem6  31584  msrf  31717  elmsta  31723  mthmpps  31757  mclsppslem  31758  mclspps  31759  scutun12  32194  scutf  32196  slerec  32200  sltrec  32201  madeval2  32213  iblabsnclem  33755  dvasin  33778  isbnd3  33865  heiborlem3  33894  iccbnd  33921  rngohomf  34047  idlss  34097  lshplss  34740  opoccl  34953  opococ  34954  oplecon3  34958  hloml  35116  lclkrslem1  37297  lclkrslem2  37298  eliccre  40200  eliocre  40206  icoiccdif  40222  limccog  40324  lptioo1  40336  cncfiooicclem1  40578  ditgeqiooicc  40648  stoweidlem30  40719  stoweidlem31  40720  stoweidlem38  40727  stoweidlem44  40733  fourierdlem26  40822  fourierdlem32  40828  fourierdlem33  40829  fourierdlem37  40833  fourierdlem42  40838  fourierdlem54  40849  fourierdlem63  40858  fourierdlem64  40859  fourierdlem65  40860  fourierdlem69  40864  fourierdlem79  40874  fourierdlem82  40877  fourierdlem89  40884  fourierdlem90  40885  fourierdlem91  40886  fourierdlem111  40906  0sal  41012  hoidmv1lelem3  41282  smfdmss  41417  smfpimltxr  41431  sigardiv  41525  sigarcol  41528  sharhght  41529  sigaradd  41530  cevathlem1  41531  cevathlem2  41532  cevath  41533  proththd  42010  perfectALTVlem2  42110
  Copyright terms: Public domain W3C validator