Theorem simp3d 1143

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 1137	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜃)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  simp3bi  1146  f1dom3fv3dif  7138  f1dom3el3dif  7139  oeeui  8418  resixp  8704  domssex2  8906  cantnflem1c  9423  cantnflem1  9425  cantnflem3  9427  cantnflem4  9428  fpwwe2lem6  10393  canthnumlem  10405  canthp1lem2  10410  wununi  10463  wunpw  10464  wunpr  10466  lelttrdi  11137  ixxdisj  13093  ixxun  13094  ixxss1  13096  ixxss2  13097  ixxss12  13098  ixxub  13099  ixxlb  13100  lbioo  13109  elicore  13130  iccsupr  13173  icodisj  13207  xov1plusxeqvd  13229  intfracq  13577  fldiv  13578  seqf1olem2  13761  cjmul  14851  icco1  15247  sumtp  15459  rpnnen2lem10  15930  ruclem2  15939  ruclem3  15940  ruclem9  15945  ruclem12  15948  dvdslegcd  16209  crth  16477  eulerthlem1  16480  eulerthlem2  16481  pcpremul  16542  prmreclem2  16616  prmreclem3  16617  4sqlem13  16656  sectcan  17465  sectco  17466  sectmon  17492  monsect  17493  funcid  17583  funcco  17584  funcsect  17585  invfuc  17690  fuciso  17691  coapm  17784  catciso  17824  postr  18036  ipodrsima  18257  psref2  18286  psasym  18292  mhm0  18436  submcl  18449  submmnd  18450  eqger  18804  eqgcpbl  18808  gaorber  18912  orbsta  18917  cayleyth  19021  pmtrrn2  19066  pmtrfinv  19067  pmtrfmvdn0  19068  dfod2  19169  sylow2blem1  19223  sylow2blem3  19225  dprdcntz  19609  dprddisj  19610  dprdffsupp  19615  dpjdisj  19654  ablfac1a  19670  ablfac1b  19671  lmodvsdir  20145  lmhmlin  20295  lbsind  20340  2idlcpbl  20503  assasca  21067  mpfind  21315  mdetunilem2  21760  mdetunilem5  21763  mdetunilem6  21764  mnfnei  22370  cnprcl  22394  lmcvg  22411  lmff  22450  lmcls  22451  lmcnp  22453  fbasssin  22985  flimfil  23118  tgpconncomp  23262  tlmtrg  23339  ustssel  23355  ustincl  23357  ustdiag  23358  ustinvel  23359  ustexhalf  23360  ustfilxp  23362  tustopn  23421  tususp  23422  imasdsf1olem  23524  xmeter  23584  xmetresbl  23588  tmstopn  23639  metustexhalf  23710  nlmnrg  23841  qdensere  23931  blcvx  23959  tgqioo  23961  icccmplem1  23983  icccmplem2  23984  reconnlem1  23987  cnmpopc  24089  iccpnfcnv  24105  phtpcer  24156  phtpcco2  24160  pcohtpy  24181  pcorev2  24189  pcophtb  24190  om1addcl  24194  pi1blem  24200  pi1cpbl  24205  pi1grplem  24210  pi1inv  24213  pi1xfrf  24214  pi1xfr  24216  pi1xfrcnvlem  24217  pi1cof  24220  pi1coghm  24222  cphreccllem  24340  cphsca  24341  cphsubrg  24342  cphsqrtcl2  24348  phclm  24394  tcphcph  24399  lmmcvg  24423  cmetcaulem  24450  lmcau  24475  bcthlem3  24488  bcthlem4  24489  minveclem4c  24587  minveclem2  24588  minveclem3b  24590  minveclem4  24594  minveclem6  24596  ivthicc  24620  ovollb2lem  24650  ovolshftlem1  24671  ovolscalem1  24675  ovolicc1  24678  ovolicc2lem2  24680  ovolicc2lem3  24681  ovolicc2lem4  24682  ovolicc2lem5  24683  ioombl1lem1  24720  dyadmaxlem  24759  volivth  24769  vitalilem2  24771  vitalilem4  24773  i1fima2  24841  itg2monolem1  24913  itgcnlem  24952  itgrevallem1  24957  itgreval  24959  itgle  24972  ibladd  24983  iblabslem  24990  itgspliticc  24999  itgsplitioo  25000  ditgcl  25020  ditgswap  25021  ditgsplitlem  25022  limcdif  25038  limcresi  25047  limcres  25048  limccnp  25053  limccnp2  25054  limcun  25057  dvlip  25155  dvlip2  25157  dveq0  25162  dvgt0lem1  25164  dvivthlem1  25170  dvcnvrelem1  25179  dvcnvre  25181  dvfsumlem2  25189  ftc1lem1  25197  ftc1lem2  25198  ftc1a  25199  ftc1lem4  25201  ftc2  25206  ftc2ditglem  25207  itgsubstlem  25210  ply1rem  25326  fta1glem2  25329  ig1pdvds  25339  plyrem  25463  fta1lem  25465  vieta1lem2  25469  aaliou3lem3  25502  pserulm  25579  psercnlem2  25581  psercnlem1  25582  psercn  25583  pserdvlem1  25584  pserdvlem2  25585  abelth2  25599  coseq00topi  25657  coseq0negpitopi  25658  cosordlem  25684  tanord1  25691  efif1olem1  25696  dvloglem  25801  efopnlem1  25809  logreclem  25910  relogbval  25920  nnlogbexp  25929  logbrec  25930  chordthmlem4  25983  quart1  26004  quartlem2  26006  quartlem3  26007  quart  26009  acosbnd  26048  atancj  26058  atanlogsublem  26063  atantan  26071  atanbndlem  26073  atans2  26079  dvatan  26083  atantayl  26085  divsqrtsumlem  26127  ftalem5  26224  basellem5  26232  ppisval  26251  chtleppi  26356  chpchtsum  26365  chpub  26366  mersenne  26373  perfectlem2  26376  dchrinv  26407  rplogsumlem2  26631  chpdifbndlem1  26699  pntibndlem2  26737  pntlema  26742  pntlemb  26743  pntlemg  26744  pntlemh  26745  pntlemr  26748  pntlemj  26749  pntlemf  26751  pntlemk  26752  pntlemo  26753  pntlemp  26756  pntleml  26757  abvcxp  26761  ostth2lem2  26780  axtgcont1  26827  cgr3simp3  26881  legso  26958  hlln  26966  hltr  26969  btwnhl  26973  mirhl  27038  mirbtwnhl  27039  opphllem4  27109  opphl  27113  hlpasch  27115  cgracgr  27177  cgraswap  27179  cgrahl  27186  cgracol  27187  inagswap  27200  inagne3  27203  dfcgrg2  27222  umgrnloopv  27474  umgredgne  27513  usgrnloopvALT  27566  frusgrnn0  27936  cusgrm1rusgr  27947  upgrclwlkcompim  28145  2wlkdlem6  28292  2wlkond  28298  2trlond  28300  numclwwlk2lem1  28736  numclwlk2lem2f1o  28739  tncp  28836  grpolidinv  28859  nvs  29021  nvz  29027  nvtri  29028  sspn  29094  minvecolem2  29233  minvecolem4c  29237  minvecolem4  29238  minvecolem5  29239  minvecolem6  29240  adj1  30291  eliccelico  31094  elicoelioo  31095  prmdvdsbc  31126  pmtrto1cl  31362  cyc3evpm  31413  slmdvsdir  31465  slmd0vs  31473  nsgqusf1olem3  31596  prmidl  31611  prmidlc  31620  qsidomlem2  31625  mxidlmax  31633  locfinreflem  31786  cnre2csqlem  31856  sigaclci  32096  unelsiga  32098  insiga  32101  unelldsys  32122  ldsysgenld  32124  sigapildsys  32126  ldgenpisyslem1  32127  measvun  32173  cntmeas  32190  sibfima  32301  signstfveq0  32552  tg5segofs  32649  bnj1018g  32939  bnj1018  32940  pfxwlk  33081  revwlk  33082  spthcycl  33087  acycgrcycl  33105  subfacp1lem3  33140  subfacp1lem4  33141  subfacp1lem5  33142  sconnpht2  33196  sconnpi1  33197  txsconn  33199  resconn  33204  cvmcn  33220  cvmsuni  33227  cvmsdisj  33228  cvmshmeo  33229  cvmlift2lem8  33268  cvmlift2lem13  33273  cvmliftphtlem  33275  cvmliftpht  33276  cvmlift3lem6  33282  msrf  33500  elmsta  33506  mthmpps  33540  mclsppslem  33541  scutun12  34000  slerec  34009  cofcut2  34087  cofcutr  34088  cofcutrtime  34089  ivthALT  34520  relowlssretop  35530  ibladdnc  35830  iblabsnclem  35836  ftc2nc  35855  dvasin  35857  isbndx  35936  isbnd3  35938  prdsbnd  35947  heiborlem3  35967  iccbnd  35994  rngohomadd  36123  rngohommul  36124  idladdcl  36173  idllmulcl  36174  idlrmulcl  36175  maxidlmax  36197  pridlc  36225  eqvreltr  36716  lshpnelb  36994  lshpcmp  36998  oplecon3  37209  opnoncon  37218  hlcvl  37369  dochshpncl  39394  lclkrslem1  39547  lclkrslem2  39548  fzne2d  39986  sticksstones3  40101  metakunt8  40129  metakunt20  40141  metakunt21  40142  metakunt22  40143  metakunt24  40145  metakunt25  40146  evlsval3  40269  flt4lem5f  40491  flt4lem7  40493  nna4b4nsq  40494  acongrep  40799  ntrneinex  41657  neicvgmex  41697  gneispace0nelrn  41720  cvgdvgrat  41901  binomcxplemdvbinom  41941  eliocre  43018  iccshift  43027  iccsuble  43028  icoiccdif  43033  mullimc  43128  limccog  43132  limciccioolb  43133  mullimcf  43135  limcperiod  43140  lptioo2  43143  lptioo1  43144  neglimc  43159  addlimc  43160  0ellimcdiv  43161  reclimc  43165  xlimmnfvlem1  43344  xlimpnfvlem1  43348  icccncfext  43399  cncfioobdlem  43408  ditgeqiooicc  43472  iblspltprt  43485  iblcncfioo  43490  itgiccshift  43492  itgperiod  43493  itgsbtaddcnst  43494  stoweidlem11  43523  stoweidlem31  43543  stoweidlem36  43548  stoweidlem38  43550  stoweidlem62  43574  dirkercncflem1  43615  dirkercncflem4  43618  fourierdlem26  43645  fourierdlem32  43651  fourierdlem33  43652  fourierdlem37  43656  fourierdlem42  43661  fourierdlem54  43672  fourierdlem63  43681  fourierdlem64  43682  fourierdlem65  43683  fourierdlem74  43692  fourierdlem75  43693  fourierdlem79  43697  fourierdlem81  43699  fourierdlem82  43700  fourierdlem89  43707  fourierdlem90  43708  fourierdlem91  43709  fourierdlem93  43711  fourierdlem101  43719  fourierdlem107  43725  fourierdlem109  43727  fourierdlem111  43729  salunicl  43828  saluncl  43829  hoidmv1lelem1  44100  hoidmv1lelem3  44102  hoidmvlelem1  44104  ovolval3  44156  iinhoiicclem  44182  smfpreimalt  44235  smfpreimaltf  44240  smfpreimale  44258  issmfgt  44260  smfpreimagt  44265  smfpreimage  44285  sigardiv  44345  sigarcol  44348  sharhght  44349  sigaradd  44350  cevathlem1  44351  cevathlem2  44352  cevath  44353  proththd  45035  perfectALTVlem2  45143