Theorem simp3d 1140

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simp3bi  1143  f1dom3fv3dif  7026  f1dom3el3dif  7027  oeeui  8228  resixp  8497  domssex2  8677  cantnflem1c  9150  cantnflem1  9152  cantnflem3  9154  cantnflem4  9155  fpwwe2lem7  10058  canthnumlem  10070  canthp1lem2  10075  wununi  10128  wunpw  10129  wunpr  10131  lelttrdi  10802  ixxdisj  12754  ixxun  12755  ixxss1  12757  ixxss2  12758  ixxss12  12759  ixxub  12760  ixxlb  12761  lbioo  12770  elicore  12790  iccsupr  12831  icodisj  12863  xov1plusxeqvd  12885  intfracq  13228  fldiv  13229  seqf1olem2  13411  cjmul  14501  icco1  14897  sumtp  15104  rpnnen2lem10  15576  ruclem2  15585  ruclem3  15586  ruclem9  15591  ruclem12  15594  dvdslegcd  15853  crth  16115  eulerthlem1  16118  eulerthlem2  16119  pcpremul  16180  prmreclem2  16253  prmreclem3  16254  4sqlem13  16293  sectcan  17025  sectco  17026  sectmon  17052  monsect  17053  funcid  17140  funcco  17141  funcsect  17142  invfuc  17244  fuciso  17245  coapm  17331  catciso  17367  postr  17563  ipodrsima  17775  psref2  17814  psasym  17820  mhm0  17964  submcl  17977  submmnd  17978  eqger  18330  eqgcpbl  18334  gaorber  18438  orbsta  18443  cayleyth  18543  pmtrrn2  18588  pmtrfinv  18589  pmtrfmvdn0  18590  dfod2  18691  sylow2blem1  18745  sylow2blem3  18747  dprdcntz  19130  dprddisj  19131  dprdffsupp  19136  dpjdisj  19175  ablfac1a  19191  ablfac1b  19192  lmodvsdir  19658  lmhmlin  19807  lbsind  19852  2idlcpbl  20007  assasca  20094  mpfind  20320  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  mnfnei  21829  cnprcl  21853  lmcvg  21870  lmff  21909  lmcls  21910  lmcnp  21912  fbasssin  22444  flimfil  22577  tgpconncomp  22721  tlmtrg  22798  ustssel  22814  ustincl  22816  ustdiag  22817  ustinvel  22818  ustexhalf  22819  ustfilxp  22821  tustopn  22880  tususp  22881  imasdsf1olem  22983  xmeter  23043  xmetresbl  23047  tmstopn  23095  metustexhalf  23166  nlmnrg  23288  qdensere  23378  blcvx  23406  tgqioo  23408  icccmplem1  23430  icccmplem2  23431  reconnlem1  23434  cnmpopc  23532  iccpnfcnv  23548  phtpcer  23599  phtpcco2  23603  pcohtpy  23624  pcorev2  23632  pcophtb  23633  om1addcl  23637  pi1blem  23643  pi1cpbl  23648  pi1grplem  23653  pi1inv  23656  pi1xfrf  23657  pi1xfr  23659  pi1xfrcnvlem  23660  pi1cof  23663  pi1coghm  23665  cphreccllem  23782  cphsca  23783  cphsubrg  23784  cphsqrtcl2  23790  phclm  23835  tcphcph  23840  lmmcvg  23864  cmetcaulem  23891  lmcau  23916  bcthlem3  23929  bcthlem4  23930  minveclem4c  24028  minveclem2  24029  minveclem3b  24031  minveclem4  24035  minveclem6  24037  ivthicc  24059  ovollb2lem  24089  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ovolicc2lem2  24119  ovolicc2lem3  24120  ovolicc2lem4  24121  ovolicc2lem5  24122  ioombl1lem1  24159  dyadmaxlem  24198  volivth  24208  vitalilem2  24210  vitalilem4  24212  i1fima2  24280  itg2monolem1  24351  itgcnlem  24390  itgrevallem1  24395  itgreval  24397  itgle  24410  ibladd  24421  iblabslem  24428  itgspliticc  24437  itgsplitioo  24438  ditgcl  24456  ditgswap  24457  ditgsplitlem  24458  limcdif  24474  limcresi  24483  limcres  24484  limccnp  24489  limccnp2  24490  limcun  24493  dvlip  24590  dvlip2  24592  dveq0  24597  dvgt0lem1  24599  dvivthlem1  24605  dvcnvrelem1  24614  dvcnvre  24616  dvfsumlem2  24624  ftc1lem1  24632  ftc1lem2  24633  ftc1a  24634  ftc1lem4  24636  ftc2  24641  ftc2ditglem  24642  itgsubstlem  24645  ply1rem  24757  fta1glem2  24760  ig1pdvds  24770  plyrem  24894  fta1lem  24896  vieta1lem2  24900  aaliou3lem3  24933  pserulm  25010  psercnlem2  25012  psercnlem1  25013  psercn  25014  pserdvlem1  25015  pserdvlem2  25016  abelth2  25030  coseq00topi  25088  coseq0negpitopi  25089  cosordlem  25115  tanord1  25121  efif1olem1  25126  dvloglem  25231  efopnlem1  25239  logreclem  25340  relogbval  25350  nnlogbexp  25359  logbrec  25360  chordthmlem4  25413  quart1  25434  quartlem2  25436  quartlem3  25437  quart  25439  acosbnd  25478  atancj  25488  atanlogsublem  25493  atantan  25501  atanbndlem  25503  atans2  25509  dvatan  25513  atantayl  25515  divsqrtsumlem  25557  ftalem5  25654  basellem5  25662  ppisval  25681  chtleppi  25786  chpchtsum  25795  chpub  25796  mersenne  25803  perfectlem2  25806  dchrinv  25837  rplogsumlem2  26061  chpdifbndlem1  26129  pntibndlem2  26167  pntlema  26172  pntlemb  26173  pntlemg  26174  pntlemh  26175  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntlemp  26186  pntleml  26187  abvcxp  26191  ostth2lem2  26210  axtgcont1  26254  cgr3simp3  26308  legso  26385  hlln  26393  hltr  26396  btwnhl  26400  mirhl  26465  mirbtwnhl  26466  opphllem4  26536  opphl  26540  hlpasch  26542  cgracgr  26604  cgraswap  26606  cgrahl  26613  cgracol  26614  inagswap  26627  inagne3  26630  dfcgrg2  26649  umgrnloopv  26891  umgredgne  26930  usgrnloopvALT  26983  frusgrnn0  27353  cusgrm1rusgr  27364  upgrclwlkcompim  27562  2wlkdlem6  27710  2wlkond  27716  2trlond  27718  numclwwlk2lem1  28155  numclwlk2lem2f1o  28158  tncp  28255  grpolidinv  28278  nvs  28440  nvz  28446  nvtri  28447  sspn  28513  minvecolem2  28652  minvecolem4c  28656  minvecolem4  28657  minvecolem5  28658  minvecolem6  28659  adj1  29710  eliccelico  30500  elicoelioo  30501  prmdvdsbc  30532  pmtrto1cl  30741  cyc3evpm  30792  slmdvsdir  30844  slmd0vs  30852  prmidl  30957  prmidlc  30964  qsidomlem2  30966  mxidlmax  30974  locfinreflem  31104  cnre2csqlem  31153  sigaclci  31391  unelsiga  31393  insiga  31396  unelldsys  31417  ldsysgenld  31419  sigapildsys  31421  ldgenpisyslem1  31422  measvun  31468  cntmeas  31485  sibfima  31596  signstfveq0  31847  tg5segofs  31944  bnj1018g  32235  bnj1018  32236  pfxwlk  32370  revwlk  32371  spthcycl  32376  acycgrcycl  32394  subfacp1lem3  32429  subfacp1lem4  32430  subfacp1lem5  32431  sconnpht2  32485  sconnpi1  32486  txsconn  32488  resconn  32493  cvmcn  32509  cvmsuni  32516  cvmsdisj  32517  cvmshmeo  32518  cvmlift2lem8  32557  cvmlift2lem13  32562  cvmliftphtlem  32564  cvmliftpht  32565  cvmlift3lem6  32571  msrf  32789  elmsta  32795  mthmpps  32829  mclsppslem  32830  scutun12  33271  slerec  33277  ivthALT  33683  relowlssretop  34647  ibladdnc  34964  iblabsnclem  34970  ftc2nc  34991  dvasin  34993  isbndx  35075  isbnd3  35077  prdsbnd  35086  heiborlem3  35106  iccbnd  35133  rngohomadd  35262  rngohommul  35263  idladdcl  35312  idllmulcl  35313  idlrmulcl  35314  maxidlmax  35336  pridlc  35364  eqvreltr  35857  lshpnelb  36135  lshpcmp  36139  oplecon3  36350  opnoncon  36359  hlcvl  36510  dochshpncl  38535  lclkrslem1  38688  lclkrslem2  38689  acongrep  39626  ntrneinex  40476  neicvgmex  40516  gneispace0nelrn  40539  cvgdvgrat  40694  binomcxplemdvbinom  40734  eliocre  41834  iccshift  41843  iccsuble  41844  icoiccdif  41849  mullimc  41946  limccog  41950  limciccioolb  41951  mullimcf  41953  limcperiod  41958  lptioo2  41961  lptioo1  41962  neglimc  41977  addlimc  41978  0ellimcdiv  41979  reclimc  41983  xlimmnfvlem1  42162  xlimpnfvlem1  42166  icccncfext  42219  cncfioobdlem  42228  ditgeqiooicc  42294  iblspltprt  42307  iblcncfioo  42312  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem11  42345  stoweidlem31  42365  stoweidlem36  42370  stoweidlem38  42372  stoweidlem62  42396  dirkercncflem1  42437  dirkercncflem4  42440  fourierdlem26  42467  fourierdlem32  42473  fourierdlem33  42474  fourierdlem37  42478  fourierdlem42  42483  fourierdlem54  42494  fourierdlem63  42503  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem75  42515  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem93  42533  fourierdlem101  42541  fourierdlem107  42547  fourierdlem109  42549  fourierdlem111  42551  salunicl  42650  saluncl  42651  hoidmv1lelem1  42922  hoidmv1lelem3  42924  hoidmvlelem1  42926  ovolval3  42978  iinhoiicclem  43004  smfpreimalt  43057  smfpreimaltf  43062  smfpreimale  43080  issmfgt  43082  smfpreimagt  43087  smfpreimage  43107  sigardiv  43167  sigarcol  43170  sharhght  43171  sigaradd  43172  cevathlem1  43173  cevathlem2  43174  cevath  43175  proththd  43828  perfectALTVlem2  43936