Theorem simp3d 1162

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

Step	Hyp	Ref	Expression
1		3simp1d.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃))
2		simp3 1156	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp3bi  1165  f1dom3fv3dif  7272  f1dom3el3dif  7273  oeeui  8612  resixp  8962  domssex2  9157  cantnflem1c  9689  cantnflem1  9691  cantnflem3  9693  cantnflem4  9694  fpwwe2lem6  10722  canthnumlem  10734  canthp1lem2  10739  wununi  10792  wunpw  10793  wunpr  10795  lelttrdi  11473  ixxdisj  13492  ixxun  13493  ixxss1  13495  ixxss2  13496  ixxss12  13497  ixxub  13498  ixxlb  13499  lbioo  13508  elicore  13530  iccsupr  13574  icodisj  13608  xov1plusxeqvd  13630  intfracq  14000  fldiv  14001  seqf1olem2  14186  cjmul  15310  icco1  15708  sumtp  15916  rpnnen2lem10  16392  ruclem2  16401  ruclem3  16402  ruclem9  16407  ruclem12  16410  dvdslegcd  16675  prmdvdsbc  16903  crth  16956  eulerthlem1  16959  eulerthlem2  16960  pcpremul  17022  prmreclem2  17096  prmreclem3  17097  4sqlem13  17136  sectcan  17931  sectco  17932  sectmon  17958  monsect  17959  funcid  18046  funcco  18047  funcsect  18048  invfuc  18153  fuciso  18154  coapm  18247  catciso  18287  postr  18495  ipodrsima  18716  psref2  18745  psasym  18751  mhm0  18990  submcl  19008  submmnd  19010  eqger  19391  eqgcpbl  19395  ghmqusnsglem1  19495  ghmquskerlem1  19498  gaorber  19523  orbsta  19528  cayleyth  19630  pmtrrn2  19675  pmtrfinv  19676  pmtrfmvdn0  19677  dfod2  19779  sylow2blem1  19835  sylow2blem3  19837  dprdcntz  20225  dprddisj  20226  dprdffsupp  20231  dpjdisj  20270  ablfac1a  20286  ablfac1b  20287  lmodvsdir  21162  lmhmlin  21311  lbsind  21356  2idlcpblrng  21566  prmidl  21622  prmidlc  21630  prmidlprop  21633  qsidomlem2  21638  qsnzr  21640  evlsval3  22399  mpfind  22425  mdetunilem2  22929  mdetunilem5  22932  mdetunilem6  22933  mnfnei  23540  cnprcl  23564  lmcvg  23581  lmff  23620  lmcls  23621  lmcnp  23623  fbasssin  24156  flimfil  24289  tgpconncomp  24433  tlmtrg  24510  ustssel  24526  ustincl  24528  ustdiag  24529  ustinvel  24530  ustexhalf  24531  ustfilxp  24533  tustopn  24590  tususp  24591  imasdsf1olem  24693  xmeter  24753  xmetresbl  24757  tmstopn  24805  metustexhalf  24876  nlmnrg  24999  qdensere  25089  blcvx  25118  tgqioo  25120  icccmplem1  25143  icccmplem2  25144  reconnlem1  25147  cnmpopc  25250  iccpnfcnv  25266  phtpcer  25317  phtpcco2  25321  pcohtpy  25342  pcorev2  25350  pcophtb  25351  om1addcl  25355  pi1blem  25361  pi1cpbl  25366  pi1grplem  25371  pi1inv  25374  pi1xfrf  25375  pi1xfr  25377  pi1xfrcnvlem  25378  pi1cof  25381  pi1coghm  25383  cphreccllem  25500  cphsca  25501  cphsubrg  25502  cphsqrtcl2  25508  phclm  25554  tcphcph  25559  lmmcvg  25583  cmetcaulem  25610  lmcau  25635  bcthlem3  25648  bcthlem4  25649  minveclem4c  25747  minveclem2  25748  minveclem3b  25750  minveclem4  25754  minveclem6  25756  ivthicc  25780  ovollb2lem  25810  ovolshftlem1  25831  ovolscalem1  25835  ovolicc1  25838  ovolicc2lem2  25840  ovolicc2lem3  25841  ovolicc2lem4  25842  ovolicc2lem5  25843  ioombl1lem1  25880  dyadmaxlem  25919  volivth  25929  vitalilem2  25931  vitalilem4  25933  i1fima2  26001  itg2monolem1  26072  itgcnlem  26111  itgrevallem1  26116  itgreval  26118  itgle  26131  ibladd  26142  iblabslem  26149  itgspliticc  26158  itgsplitioo  26159  ditgcl  26179  ditgswap  26180  ditgsplitlem  26181  limcdif  26197  limcresi  26206  limcres  26207  limccnp  26212  limccnp2  26213  limcun  26216  dvlip  26314  dvlip2  26316  dveq0  26321  dvgt0lem1  26323  dvivthlem1  26329  dvcnvrelem1  26338  dvcnvre  26340  dvfsumlem2  26348  ftc1lem1  26356  ftc1lem2  26357  ftc1a  26358  ftc1lem4  26360  ftc2  26365  ftc2ditglem  26366  itgsubstlem  26369  ply1rem  26485  fta1glem2  26488  ig1pdvds  26499  plyrem  26627  fta1lem  26629  vieta1lem2  26635  aaliou3lem3  26672  pserulm  26750  psercnlem2  26752  psercnlem1  26753  psercn  26754  pserdvlem1  26755  pserdvlem2  26756  abelth2  26770  coseq00topi  26832  coseq0negpitopi  26833  cosordlem  26859  tanord1  26866  efif1olem1  26871  dvloglem  26977  efopnlem1  26985  logreclem  27091  relogbval  27101  nnlogbexp  27110  logbrec  27111  chordthmlem4  27164  quart1  27185  quartlem2  27187  quartlem3  27188  quart  27190  acosbnd  27229  atancj  27239  atanlogsublem  27244  atantan  27252  atanbndlem  27254  atans2  27260  dvatan  27264  atantayl  27266  divsqrtsumlem  27308  ftalem5  27405  basellem5  27413  ppisval  27432  chtleppi  27538  chpchtsum  27547  chpub  27548  mersenne  27555  perfectlem2  27558  dchrinv  27589  rplogsumlem2  27813  chpdifbndlem1  27881  pntibndlem2  27919  pntlema  27924  pntlemb  27925  pntlemg  27926  pntlemh  27927  pntlemr  27930  pntlemj  27931  pntlemf  27933  pntlemk  27934  pntlemo  27935  pntlemp  27938  pntleml  27939  abvcxp  27943  ostth2lem2  27962  flt4lem5f  27988  flt4lem7  27990  nna4b4nsq  27991  cutsun12  28177  lesrec  28186  eqcuts3  28191  cofcut2  28309  cofcutr  28311  cofcutrtime  28314  cutmax  28321  cutmin  28322  addsproplem5  28360  addsproplem6  28361  leadds1  28376  addsuniflem  28388  addsasslem1  28390  addsasslem2  28391  negsproplem4  28418  negsproplem6  28420  negcut2  28427  negsunif  28442  mulsproplem12  28514  sltmuls1  28534  sltmuls2  28535  mulsuniflem  28536  precsexlem11  28604  twocut  28810  pw2cut2  28849  axtgcont1  28931  cgr3simp3  28986  legso  29063  hlln  29074  hltr  29077  btwnhl  29081  tghlsub  29087  mirhl  29152  mirbtwnhl  29153  opphllem4  29227  opphl  29231  hlpasch  29235  cgracgr  29326  cgraswap  29328  cgrahl  29336  cgracol  29337  inagswap  29361  inagne3  29364  dfcgrg2  29409  umgrnloopv  29685  umgredgne  29724  usgrnloopvALT  29783  frusgrnn0  30153  cusgrm1rusgr  30164  pfxwlk  30267  revwlk  30268  upgrclwlkcompim  30369  spthcycl  30393  2wlkdlem6  30521  2wlkond  30527  2trlond  30529  acycgrcycl  30754  numclwwlk2lem1  30978  numclwlk2lem2f1o  30981  tncp  31081  grpolidinv  31104  nvs  31266  nvz  31272  nvtri  31273  sspn  31339  minvecolem2  31478  minvecolem4c  31482  minvecolem4  31483  minvecolem5  31484  minvecolem6  31485  adj1  32536  cgrahlb  33048  inagbtwn  33049  cgrgptxfr  33054  inagcgratrgncol  33058  tgextahpl  33070  tgaasne  33083  eliccelico  33412  elicoelioo  33413  pmtrto1cl  33703  cyc3evpm  33754  slmdvsdir  33820  slmd0vs  33828  sdrgdvcl  33904  sdrginvcl  33905  nsgqusf1olem3  34009  mxidlmax  34033  qsdrnglem2  34063  0ringmon1p  34132  ig1pmindeg  34177  ply1degltdimlem  34297  irngss  34362  ply1annig1p  34379  minplycl  34381  algextdeglem3  34394  algextdeglem4  34395  constrsqrtcl  34454  locfinreflem  34515  cnre2csqlem  34585  sigaclci  34807  unelsiga  34809  insiga  34813  unelldsys  34834  ldsysgenld  34836  sigapildsys  34838  ldgenpisyslem1  34839  measvun  34885  cntmeas  34902  sibfima  35013  signstfveq0  35249  cgranbtwn  35341  tg5segofs  35348  bnj1018g  35636  bnj1018  35637  subfacp1lem3  35990  subfacp1lem4  35991  subfacp1lem5  35992  sconnpht2  36046  sconnpi1  36047  txsconn  36049  resconn  36054  cvmcn  36070  cvmsuni  36077  cvmsdisj  36078  cvmshmeo  36079  cvmlift2lem8  36118  cvmlift2lem13  36123  cvmliftphtlem  36125  cvmliftpht  36126  cvmlift3lem6  36132  msrf  36350  elmsta  36356  mthmpps  36390  mclsppslem  36391  ivthALT  37166  weiunfrlem  37295  weiunfr  37298  relowlssretop  38330  ibladdnc  38639  iblabsnclem  38645  ftc2nc  38664  dvasin  38666  isbndx  38760  isbnd3  38762  prdsbnd  38771  heiborlem3  38791  iccbnd  38818  rngohomadd  38947  rngohommul  38948  idladdcl  38997  idllmulcl  38998  idlrmulcl  38999  maxidlmax  39021  pridlc  39049  eqvreltr  39667  lshpnelb  40085  lshpcmp  40089  oplecon3  40300  opnoncon  40309  hlcvl  40460  dochshpncl  42485  lclkrslem1  42638  lclkrslem2  42639  fzne2d  43074  primrootsunit1  43191  primrootscoprmpow  43193  primrootlekpowne0  43199  aks6d1c1p1  43201  aks6d1c2  43224  sticksstones3  43242  aks5lem1  43280  aks5lem2  43281  aks5lem3a  43283  acongrep  44031  ntrneinex  45121  neicvgmex  45161  gneispace0nelrn  45184  cvgdvgrat  45341  binomcxplemdvbinom  45381  eliocre  46565  iccshift  46574  iccsuble  46575  icoiccdif  46580  mullimc  46672  limccog  46676  limciccioolb  46677  mullimcf  46679  limcperiod  46684  lptioo2  46687  lptioo1  46688  neglimc  46701  addlimc  46702  0ellimcdiv  46703  reclimc  46707  xlimmnfvlem1  46886  xlimpnfvlem1  46890  icccncfext  46941  cncfioobdlem  46950  ditgeqiooicc  47014  iblspltprt  47027  iblcncfioo  47032  itgiccshift  47034  itgperiod  47035  itgsbtaddcnst  47036  stoweidlem11  47065  stoweidlem31  47085  stoweidlem36  47090  stoweidlem38  47092  stoweidlem62  47116  dirkercncflem1  47157  dirkercncflem4  47160  fourierdlem26  47187  fourierdlem32  47193  fourierdlem33  47194  fourierdlem37  47198  fourierdlem42  47203  fourierdlem54  47214  fourierdlem63  47223  fourierdlem64  47224  fourierdlem65  47225  fourierdlem74  47234  fourierdlem75  47235  fourierdlem79  47239  fourierdlem81  47241  fourierdlem82  47242  fourierdlem89  47249  fourierdlem90  47250  fourierdlem91  47251  fourierdlem93  47253  fourierdlem101  47261  fourierdlem107  47267  fourierdlem109  47269  fourierdlem111  47271  salunicl  47370  saluncl  47371  hoidmv1lelem1  47645  hoidmv1lelem3  47647  hoidmvlelem1  47649  ovolval3  47701  iinhoiicclem  47727  smfpreimalt  47785  smfpreimaltf  47790  smfpreimale  47808  issmfgt  47810  smfpreimagt  47816  smfpreimage  47836  sigardiv  47915  sigarcol  47918  sharhght  47919  sigaradd  47920  cevathlem1  47921  cevathlem2  47922  cevath  47923  proththd  48743  perfectALTVlem2  48864  gpgnbgrvtx0  49216  gpgnbgrvtx1  49217  imasubc2  50304  imaf1co  50307  idfullsubc  50313  fucofulem1  50462  rr3fv3cld  50993