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

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

Proof of Theorem simp3d
StepHypRef Expression
1 3simp1d.1 . 2 (𝜑 → (𝜓𝜒𝜃))
2 simp3 1138 . 2 ((𝜓𝜒𝜃) → 𝜃)
31, 2syl 17 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1087
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 206  df-an 397  df-3an 1089
This theorem is referenced by:  simp3bi  1147  f1dom3fv3dif  7211  f1dom3el3dif  7212  oeeui  8541  resixp  8829  domssex2  9039  cantnflem1c  9581  cantnflem1  9583  cantnflem3  9585  cantnflem4  9586  fpwwe2lem6  10530  canthnumlem  10542  canthp1lem2  10547  wununi  10600  wunpw  10601  wunpr  10603  lelttrdi  11275  ixxdisj  13233  ixxun  13234  ixxss1  13236  ixxss2  13237  ixxss12  13238  ixxub  13239  ixxlb  13240  lbioo  13249  elicore  13270  iccsupr  13313  icodisj  13347  xov1plusxeqvd  13369  intfracq  13718  fldiv  13719  seqf1olem2  13902  cjmul  14987  icco1  15382  sumtp  15594  rpnnen2lem10  16065  ruclem2  16074  ruclem3  16075  ruclem9  16080  ruclem12  16083  dvdslegcd  16344  crth  16610  eulerthlem1  16613  eulerthlem2  16614  pcpremul  16675  prmreclem2  16749  prmreclem3  16750  4sqlem13  16789  sectcan  17598  sectco  17599  sectmon  17625  monsect  17626  funcid  17716  funcco  17717  funcsect  17718  invfuc  17823  fuciso  17824  coapm  17917  catciso  17957  postr  18169  ipodrsima  18390  psref2  18419  psasym  18425  mhm0  18570  submcl  18583  submmnd  18584  eqger  18939  eqgcpbl  18943  gaorber  19047  orbsta  19052  cayleyth  19156  pmtrrn2  19201  pmtrfinv  19202  pmtrfmvdn0  19203  dfod2  19305  sylow2blem1  19361  sylow2blem3  19363  dprdcntz  19746  dprddisj  19747  dprdffsupp  19752  dpjdisj  19791  ablfac1a  19807  ablfac1b  19808  lmodvsdir  20299  lmhmlin  20449  lbsind  20494  2idlcpbl  20657  assasca  21221  mpfind  21469  mdetunilem2  21914  mdetunilem5  21917  mdetunilem6  21918  mnfnei  22524  cnprcl  22548  lmcvg  22565  lmff  22604  lmcls  22605  lmcnp  22607  fbasssin  23139  flimfil  23272  tgpconncomp  23416  tlmtrg  23493  ustssel  23509  ustincl  23511  ustdiag  23512  ustinvel  23513  ustexhalf  23514  ustfilxp  23516  tustopn  23575  tususp  23576  imasdsf1olem  23678  xmeter  23738  xmetresbl  23742  tmstopn  23793  metustexhalf  23864  nlmnrg  23995  qdensere  24085  blcvx  24113  tgqioo  24115  icccmplem1  24137  icccmplem2  24138  reconnlem1  24141  cnmpopc  24243  iccpnfcnv  24259  phtpcer  24310  phtpcco2  24314  pcohtpy  24335  pcorev2  24343  pcophtb  24344  om1addcl  24348  pi1blem  24354  pi1cpbl  24359  pi1grplem  24364  pi1inv  24367  pi1xfrf  24368  pi1xfr  24370  pi1xfrcnvlem  24371  pi1cof  24374  pi1coghm  24376  cphreccllem  24494  cphsca  24495  cphsubrg  24496  cphsqrtcl2  24502  phclm  24548  tcphcph  24553  lmmcvg  24577  cmetcaulem  24604  lmcau  24629  bcthlem3  24642  bcthlem4  24643  minveclem4c  24741  minveclem2  24742  minveclem3b  24744  minveclem4  24748  minveclem6  24750  ivthicc  24774  ovollb2lem  24804  ovolshftlem1  24825  ovolscalem1  24829  ovolicc1  24832  ovolicc2lem2  24834  ovolicc2lem3  24835  ovolicc2lem4  24836  ovolicc2lem5  24837  ioombl1lem1  24874  dyadmaxlem  24913  volivth  24923  vitalilem2  24925  vitalilem4  24927  i1fima2  24995  itg2monolem1  25067  itgcnlem  25106  itgrevallem1  25111  itgreval  25113  itgle  25126  ibladd  25137  iblabslem  25144  itgspliticc  25153  itgsplitioo  25154  ditgcl  25174  ditgswap  25175  ditgsplitlem  25176  limcdif  25192  limcresi  25201  limcres  25202  limccnp  25207  limccnp2  25208  limcun  25211  dvlip  25309  dvlip2  25311  dveq0  25316  dvgt0lem1  25318  dvivthlem1  25324  dvcnvrelem1  25333  dvcnvre  25335  dvfsumlem2  25343  ftc1lem1  25351  ftc1lem2  25352  ftc1a  25353  ftc1lem4  25355  ftc2  25360  ftc2ditglem  25361  itgsubstlem  25364  ply1rem  25480  fta1glem2  25483  ig1pdvds  25493  plyrem  25617  fta1lem  25619  vieta1lem2  25623  aaliou3lem3  25656  pserulm  25733  psercnlem2  25735  psercnlem1  25736  psercn  25737  pserdvlem1  25738  pserdvlem2  25739  abelth2  25753  coseq00topi  25811  coseq0negpitopi  25812  cosordlem  25838  tanord1  25845  efif1olem1  25850  dvloglem  25955  efopnlem1  25963  logreclem  26064  relogbval  26074  nnlogbexp  26083  logbrec  26084  chordthmlem4  26137  quart1  26158  quartlem2  26160  quartlem3  26161  quart  26163  acosbnd  26202  atancj  26212  atanlogsublem  26217  atantan  26225  atanbndlem  26227  atans2  26233  dvatan  26237  atantayl  26239  divsqrtsumlem  26281  ftalem5  26378  basellem5  26386  ppisval  26405  chtleppi  26510  chpchtsum  26519  chpub  26520  mersenne  26527  perfectlem2  26530  dchrinv  26561  rplogsumlem2  26785  chpdifbndlem1  26853  pntibndlem2  26891  pntlema  26896  pntlemb  26897  pntlemg  26898  pntlemh  26899  pntlemr  26902  pntlemj  26903  pntlemf  26905  pntlemk  26906  pntlemo  26907  pntlemp  26910  pntleml  26911  abvcxp  26915  ostth2lem2  26934  scutun12  27101  slerec  27110  cofcut2  27190  cofcutr  27192  cofcutrtime  27195  axtgcont1  27239  cgr3simp3  27293  legso  27370  hlln  27378  hltr  27381  btwnhl  27385  mirhl  27450  mirbtwnhl  27451  opphllem4  27521  opphl  27525  hlpasch  27527  cgracgr  27589  cgraswap  27591  cgrahl  27598  cgracol  27599  inagswap  27612  inagne3  27615  dfcgrg2  27634  umgrnloopv  27886  umgredgne  27925  usgrnloopvALT  27978  frusgrnn0  28348  cusgrm1rusgr  28359  upgrclwlkcompim  28558  2wlkdlem6  28705  2wlkond  28711  2trlond  28713  numclwwlk2lem1  29149  numclwlk2lem2f1o  29152  tncp  29249  grpolidinv  29272  nvs  29434  nvz  29440  nvtri  29441  sspn  29507  minvecolem2  29646  minvecolem4c  29650  minvecolem4  29651  minvecolem5  29652  minvecolem6  29653  adj1  30704  eliccelico  31506  elicoelioo  31507  prmdvdsbc  31538  pmtrto1cl  31774  cyc3evpm  31825  slmdvsdir  31877  slmd0vs  31885  sdrgdvcl  31902  sdrginvcl  31903  nsgqusf1olem3  32019  prmidl  32034  prmidlc  32043  qsidomlem2  32048  mxidlmax  32056  0ringmon1p  32086  irngss  32181  locfinreflem  32233  cnre2csqlem  32303  sigaclci  32543  unelsiga  32545  insiga  32548  unelldsys  32569  ldsysgenld  32571  sigapildsys  32573  ldgenpisyslem1  32574  measvun  32620  cntmeas  32637  sibfima  32750  signstfveq0  33001  tg5segofs  33098  bnj1018g  33387  bnj1018  33388  pfxwlk  33529  revwlk  33530  spthcycl  33535  acycgrcycl  33553  subfacp1lem3  33588  subfacp1lem4  33589  subfacp1lem5  33590  sconnpht2  33644  sconnpi1  33645  txsconn  33647  resconn  33652  cvmcn  33668  cvmsuni  33675  cvmsdisj  33676  cvmshmeo  33677  cvmlift2lem8  33716  cvmlift2lem13  33721  cvmliftphtlem  33723  cvmliftpht  33724  cvmlift3lem6  33730  msrf  33948  elmsta  33954  mthmpps  33988  mclsppslem  33989  addsproplem5  34288  addsproplem6  34289  sleadd1  34301  addsunif  34307  addsasslem1  34308  addsasslem2  34309  negsproplem4  34324  negsproplem6  34326  negscut2  34333  ivthALT  34745  relowlssretop  35772  ibladdnc  36073  iblabsnclem  36079  ftc2nc  36098  dvasin  36100  isbndx  36179  isbnd3  36181  prdsbnd  36190  heiborlem3  36210  iccbnd  36237  rngohomadd  36366  rngohommul  36367  idladdcl  36416  idllmulcl  36417  idlrmulcl  36418  maxidlmax  36440  pridlc  36468  eqvreltr  37007  lshpnelb  37384  lshpcmp  37388  oplecon3  37599  opnoncon  37608  hlcvl  37759  dochshpncl  39785  lclkrslem1  39938  lclkrslem2  39939  fzne2d  40376  sticksstones3  40494  metakunt8  40522  metakunt20  40534  metakunt21  40535  metakunt22  40536  metakunt24  40538  metakunt25  40539  evlsval3  40667  flt4lem5f  40904  flt4lem7  40906  nna4b4nsq  40907  acongrep  41213  ntrneinex  42260  neicvgmex  42300  gneispace0nelrn  42323  cvgdvgrat  42504  binomcxplemdvbinom  42544  eliocre  43648  iccshift  43657  iccsuble  43658  icoiccdif  43663  mullimc  43758  limccog  43762  limciccioolb  43763  mullimcf  43765  limcperiod  43770  lptioo2  43773  lptioo1  43774  neglimc  43789  addlimc  43790  0ellimcdiv  43791  reclimc  43795  xlimmnfvlem1  43974  xlimpnfvlem1  43978  icccncfext  44029  cncfioobdlem  44038  ditgeqiooicc  44102  iblspltprt  44115  iblcncfioo  44120  itgiccshift  44122  itgperiod  44123  itgsbtaddcnst  44124  stoweidlem11  44153  stoweidlem31  44173  stoweidlem36  44178  stoweidlem38  44180  stoweidlem62  44204  dirkercncflem1  44245  dirkercncflem4  44248  fourierdlem26  44275  fourierdlem32  44281  fourierdlem33  44282  fourierdlem37  44286  fourierdlem42  44291  fourierdlem54  44302  fourierdlem63  44311  fourierdlem64  44312  fourierdlem65  44313  fourierdlem74  44322  fourierdlem75  44323  fourierdlem79  44327  fourierdlem81  44329  fourierdlem82  44330  fourierdlem89  44337  fourierdlem90  44338  fourierdlem91  44339  fourierdlem93  44341  fourierdlem101  44349  fourierdlem107  44355  fourierdlem109  44357  fourierdlem111  44359  salunicl  44458  saluncl  44459  hoidmv1lelem1  44733  hoidmv1lelem3  44735  hoidmvlelem1  44737  ovolval3  44789  iinhoiicclem  44815  smfpreimalt  44873  smfpreimaltf  44878  smfpreimale  44896  issmfgt  44898  smfpreimagt  44904  smfpreimage  44924  sigardiv  45003  sigarcol  45006  sharhght  45007  sigaradd  45008  cevathlem1  45009  cevathlem2  45010  cevath  45011  proththd  45707  perfectALTVlem2  45815
  Copyright terms: Public domain W3C validator