Theorem simp3d 1142

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  simp3bi  1145  f1dom3fv3dif  7269  f1dom3el3dif  7270  oeeui  8604  resixp  8929  domssex2  9139  cantnflem1c  9684  cantnflem1  9686  cantnflem3  9688  cantnflem4  9689  fpwwe2lem6  10633  canthnumlem  10645  canthp1lem2  10650  wununi  10703  wunpw  10704  wunpr  10706  lelttrdi  11380  ixxdisj  13343  ixxun  13344  ixxss1  13346  ixxss2  13347  ixxss12  13348  ixxub  13349  ixxlb  13350  lbioo  13359  elicore  13380  iccsupr  13423  icodisj  13457  xov1plusxeqvd  13479  intfracq  13828  fldiv  13829  seqf1olem2  14012  cjmul  15093  icco1  15488  sumtp  15699  rpnnen2lem10  16170  ruclem2  16179  ruclem3  16180  ruclem9  16185  ruclem12  16188  dvdslegcd  16449  crth  16715  eulerthlem1  16718  eulerthlem2  16719  pcpremul  16780  prmreclem2  16854  prmreclem3  16855  4sqlem13  16894  sectcan  17706  sectco  17707  sectmon  17733  monsect  17734  funcid  17824  funcco  17825  funcsect  17826  invfuc  17931  fuciso  17932  coapm  18025  catciso  18065  postr  18277  ipodrsima  18498  psref2  18527  psasym  18533  mhm0  18716  submcl  18729  submmnd  18730  eqger  19094  eqgcpbl  19098  gaorber  19213  orbsta  19218  cayleyth  19324  pmtrrn2  19369  pmtrfinv  19370  pmtrfmvdn0  19371  dfod2  19473  sylow2blem1  19529  sylow2blem3  19531  dprdcntz  19919  dprddisj  19920  dprdffsupp  19925  dpjdisj  19964  ablfac1a  19980  ablfac1b  19981  lmodvsdir  20640  lmhmlin  20790  lbsind  20835  2idlcpblrng  21020  mpfind  21889  mdetunilem2  22335  mdetunilem5  22338  mdetunilem6  22339  mnfnei  22945  cnprcl  22969  lmcvg  22986  lmff  23025  lmcls  23026  lmcnp  23028  fbasssin  23560  flimfil  23693  tgpconncomp  23837  tlmtrg  23914  ustssel  23930  ustincl  23932  ustdiag  23933  ustinvel  23934  ustexhalf  23935  ustfilxp  23937  tustopn  23996  tususp  23997  imasdsf1olem  24099  xmeter  24159  xmetresbl  24163  tmstopn  24214  metustexhalf  24285  nlmnrg  24416  qdensere  24506  blcvx  24534  tgqioo  24536  icccmplem1  24558  icccmplem2  24559  reconnlem1  24562  cnmpopc  24669  iccpnfcnv  24689  phtpcer  24741  phtpcco2  24746  pcohtpy  24767  pcorev2  24775  pcophtb  24776  om1addcl  24780  pi1blem  24786  pi1cpbl  24791  pi1grplem  24796  pi1inv  24799  pi1xfrf  24800  pi1xfr  24802  pi1xfrcnvlem  24803  pi1cof  24806  pi1coghm  24808  cphreccllem  24926  cphsca  24927  cphsubrg  24928  cphsqrtcl2  24934  phclm  24980  tcphcph  24985  lmmcvg  25009  cmetcaulem  25036  lmcau  25061  bcthlem3  25074  bcthlem4  25075  minveclem4c  25173  minveclem2  25174  minveclem3b  25176  minveclem4  25180  minveclem6  25182  ivthicc  25207  ovollb2lem  25237  ovolshftlem1  25258  ovolscalem1  25262  ovolicc1  25265  ovolicc2lem2  25267  ovolicc2lem3  25268  ovolicc2lem4  25269  ovolicc2lem5  25270  ioombl1lem1  25307  dyadmaxlem  25346  volivth  25356  vitalilem2  25358  vitalilem4  25360  i1fima2  25428  itg2monolem1  25500  itgcnlem  25539  itgrevallem1  25544  itgreval  25546  itgle  25559  ibladd  25570  iblabslem  25577  itgspliticc  25586  itgsplitioo  25587  ditgcl  25607  ditgswap  25608  ditgsplitlem  25609  limcdif  25625  limcresi  25634  limcres  25635  limccnp  25640  limccnp2  25641  limcun  25644  dvlip  25745  dvlip2  25747  dveq0  25752  dvgt0lem1  25754  dvivthlem1  25760  dvcnvrelem1  25769  dvcnvre  25771  dvfsumlem2  25779  ftc1lem1  25787  ftc1lem2  25788  ftc1a  25789  ftc1lem4  25791  ftc2  25796  ftc2ditglem  25797  itgsubstlem  25800  ply1rem  25916  fta1glem2  25919  ig1pdvds  25929  plyrem  26054  fta1lem  26056  vieta1lem2  26060  aaliou3lem3  26093  pserulm  26170  psercnlem2  26172  psercnlem1  26173  psercn  26174  pserdvlem1  26175  pserdvlem2  26176  abelth2  26190  coseq00topi  26248  coseq0negpitopi  26249  cosordlem  26275  tanord1  26282  efif1olem1  26287  dvloglem  26392  efopnlem1  26400  logreclem  26503  relogbval  26513  nnlogbexp  26522  logbrec  26523  chordthmlem4  26576  quart1  26597  quartlem2  26599  quartlem3  26600  quart  26602  acosbnd  26641  atancj  26651  atanlogsublem  26656  atantan  26664  atanbndlem  26666  atans2  26672  dvatan  26676  atantayl  26678  divsqrtsumlem  26720  ftalem5  26817  basellem5  26825  ppisval  26844  chtleppi  26949  chpchtsum  26958  chpub  26959  mersenne  26966  perfectlem2  26969  dchrinv  27000  rplogsumlem2  27224  chpdifbndlem1  27292  pntibndlem2  27330  pntlema  27335  pntlemb  27336  pntlemg  27337  pntlemh  27338  pntlemr  27341  pntlemj  27342  pntlemf  27344  pntlemk  27345  pntlemo  27346  pntlemp  27349  pntleml  27350  abvcxp  27354  ostth2lem2  27373  scutun12  27548  slerec  27557  cofcut2  27647  cofcutr  27649  cofcutrtime  27652  addsproplem5  27695  addsproplem6  27696  sleadd1  27711  addsuniflem  27723  addsasslem1  27725  addsasslem2  27726  negsproplem4  27744  negsproplem6  27746  negscut2  27753  negsunif  27768  mulsproplem12  27822  ssltmul1  27841  ssltmul2  27842  mulsuniflem  27843  precsexlem11  27902  axtgcont1  27986  cgr3simp3  28040  legso  28117  hlln  28125  hltr  28128  btwnhl  28132  mirhl  28197  mirbtwnhl  28198  opphllem4  28268  opphl  28272  hlpasch  28274  cgracgr  28336  cgraswap  28338  cgrahl  28345  cgracol  28346  inagswap  28359  inagne3  28362  dfcgrg2  28381  umgrnloopv  28633  umgredgne  28672  usgrnloopvALT  28725  frusgrnn0  29095  cusgrm1rusgr  29106  upgrclwlkcompim  29305  2wlkdlem6  29452  2wlkond  29458  2trlond  29460  numclwwlk2lem1  29896  numclwlk2lem2f1o  29899  tncp  29998  grpolidinv  30021  nvs  30183  nvz  30189  nvtri  30190  sspn  30256  minvecolem2  30395  minvecolem4c  30399  minvecolem4  30400  minvecolem5  30401  minvecolem6  30402  adj1  31453  eliccelico  32255  elicoelioo  32256  prmdvdsbc  32289  pmtrto1cl  32528  cyc3evpm  32579  slmdvsdir  32631  slmd0vs  32639  sdrgdvcl  32667  sdrginvcl  32668  nsgqusf1olem3  32800  ghmquskerlem1  32802  prmidl  32832  prmidlc  32841  qsidomlem2  32846  qsnzr  32848  mxidlmax  32855  qsdrnglem2  32884  0ringmon1p  32910  ig1pmindeg  32947  ply1degltdimlem  32995  irngss  33040  ply1annig1p  33054  minplycl  33056  algextdeglem3  33064  algextdeglem4  33065  locfinreflem  33118  cnre2csqlem  33188  sigaclci  33428  unelsiga  33430  insiga  33433  unelldsys  33454  ldsysgenld  33456  sigapildsys  33458  ldgenpisyslem1  33459  measvun  33505  cntmeas  33522  sibfima  33635  signstfveq0  33886  tg5segofs  33983  bnj1018g  34272  bnj1018  34273  pfxwlk  34412  revwlk  34413  spthcycl  34418  acycgrcycl  34436  subfacp1lem3  34471  subfacp1lem4  34472  subfacp1lem5  34473  sconnpht2  34527  sconnpi1  34528  txsconn  34530  resconn  34535  cvmcn  34551  cvmsuni  34558  cvmsdisj  34559  cvmshmeo  34560  cvmlift2lem8  34599  cvmlift2lem13  34604  cvmliftphtlem  34606  cvmliftpht  34607  cvmlift3lem6  34613  msrf  34831  elmsta  34837  mthmpps  34871  mclsppslem  34872  gg-dvfsumlem2  35469  ivthALT  35523  relowlssretop  36547  ibladdnc  36848  iblabsnclem  36854  ftc2nc  36873  dvasin  36875  isbndx  36953  isbnd3  36955  prdsbnd  36964  heiborlem3  36984  iccbnd  37011  rngohomadd  37140  rngohommul  37141  idladdcl  37190  idllmulcl  37191  idlrmulcl  37192  maxidlmax  37214  pridlc  37242  eqvreltr  37780  lshpnelb  38157  lshpcmp  38161  oplecon3  38372  opnoncon  38381  hlcvl  38532  dochshpncl  40558  lclkrslem1  40711  lclkrslem2  40712  fzne2d  41152  sticksstones3  41270  metakunt8  41298  metakunt20  41310  metakunt21  41311  metakunt22  41312  metakunt24  41314  metakunt25  41315  evlsval3  41433  flt4lem5f  41701  flt4lem7  41703  nna4b4nsq  41704  acongrep  42021  ntrneinex  43130  neicvgmex  43170  gneispace0nelrn  43193  cvgdvgrat  43374  binomcxplemdvbinom  43414  eliocre  44520  iccshift  44529  iccsuble  44530  icoiccdif  44535  mullimc  44630  limccog  44634  limciccioolb  44635  mullimcf  44637  limcperiod  44642  lptioo2  44645  lptioo1  44646  neglimc  44661  addlimc  44662  0ellimcdiv  44663  reclimc  44667  xlimmnfvlem1  44846  xlimpnfvlem1  44850  icccncfext  44901  cncfioobdlem  44910  ditgeqiooicc  44974  iblspltprt  44987  iblcncfioo  44992  itgiccshift  44994  itgperiod  44995  itgsbtaddcnst  44996  stoweidlem11  45025  stoweidlem31  45045  stoweidlem36  45050  stoweidlem38  45052  stoweidlem62  45076  dirkercncflem1  45117  dirkercncflem4  45120  fourierdlem26  45147  fourierdlem32  45153  fourierdlem33  45154  fourierdlem37  45158  fourierdlem42  45163  fourierdlem54  45174  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem74  45194  fourierdlem75  45195  fourierdlem79  45199  fourierdlem81  45201  fourierdlem82  45202  fourierdlem89  45209  fourierdlem90  45210  fourierdlem91  45211  fourierdlem93  45213  fourierdlem101  45221  fourierdlem107  45227  fourierdlem109  45229  fourierdlem111  45231  salunicl  45330  saluncl  45331  hoidmv1lelem1  45605  hoidmv1lelem3  45607  hoidmvlelem1  45609  ovolval3  45661  iinhoiicclem  45687  smfpreimalt  45745  smfpreimaltf  45750  smfpreimale  45768  issmfgt  45770  smfpreimagt  45776  smfpreimage  45796  sigardiv  45875  sigarcol  45878  sharhght  45879  sigaradd  45880  cevathlem1  45881  cevathlem2  45882  cevath  45883  proththd  46580  perfectALTVlem2  46688