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

This theorem is referenced by:  simp3bi  1145  f1dom3fv3dif  7122  f1dom3el3dif  7123  oeeui  8395  resixp  8679  domssex2  8873  cantnflem1c  9375  cantnflem1  9377  cantnflem3  9379  cantnflem4  9380  fpwwe2lem6  10323  canthnumlem  10335  canthp1lem2  10340  wununi  10393  wunpw  10394  wunpr  10396  lelttrdi  11067  ixxdisj  13023  ixxun  13024  ixxss1  13026  ixxss2  13027  ixxss12  13028  ixxub  13029  ixxlb  13030  lbioo  13039  elicore  13060  iccsupr  13103  icodisj  13137  xov1plusxeqvd  13159  intfracq  13507  fldiv  13508  seqf1olem2  13691  cjmul  14781  icco1  15177  sumtp  15389  rpnnen2lem10  15860  ruclem2  15869  ruclem3  15870  ruclem9  15875  ruclem12  15878  dvdslegcd  16139  crth  16407  eulerthlem1  16410  eulerthlem2  16411  pcpremul  16472  prmreclem2  16546  prmreclem3  16547  4sqlem13  16586  sectcan  17384  sectco  17385  sectmon  17411  monsect  17412  funcid  17501  funcco  17502  funcsect  17503  invfuc  17608  fuciso  17609  coapm  17702  catciso  17742  postr  17953  ipodrsima  18174  psref2  18203  psasym  18209  mhm0  18353  submcl  18366  submmnd  18367  eqger  18721  eqgcpbl  18725  gaorber  18829  orbsta  18834  cayleyth  18938  pmtrrn2  18983  pmtrfinv  18984  pmtrfmvdn0  18985  dfod2  19086  sylow2blem1  19140  sylow2blem3  19142  dprdcntz  19526  dprddisj  19527  dprdffsupp  19532  dpjdisj  19571  ablfac1a  19587  ablfac1b  19588  lmodvsdir  20062  lmhmlin  20212  lbsind  20257  2idlcpbl  20418  assasca  20979  mpfind  21227  mdetunilem2  21670  mdetunilem5  21673  mdetunilem6  21674  mnfnei  22280  cnprcl  22304  lmcvg  22321  lmff  22360  lmcls  22361  lmcnp  22363  fbasssin  22895  flimfil  23028  tgpconncomp  23172  tlmtrg  23249  ustssel  23265  ustincl  23267  ustdiag  23268  ustinvel  23269  ustexhalf  23270  ustfilxp  23272  tustopn  23331  tususp  23332  imasdsf1olem  23434  xmeter  23494  xmetresbl  23498  tmstopn  23547  metustexhalf  23618  nlmnrg  23749  qdensere  23839  blcvx  23867  tgqioo  23869  icccmplem1  23891  icccmplem2  23892  reconnlem1  23895  cnmpopc  23997  iccpnfcnv  24013  phtpcer  24064  phtpcco2  24068  pcohtpy  24089  pcorev2  24097  pcophtb  24098  om1addcl  24102  pi1blem  24108  pi1cpbl  24113  pi1grplem  24118  pi1inv  24121  pi1xfrf  24122  pi1xfr  24124  pi1xfrcnvlem  24125  pi1cof  24128  pi1coghm  24130  cphreccllem  24247  cphsca  24248  cphsubrg  24249  cphsqrtcl2  24255  phclm  24301  tcphcph  24306  lmmcvg  24330  cmetcaulem  24357  lmcau  24382  bcthlem3  24395  bcthlem4  24396  minveclem4c  24494  minveclem2  24495  minveclem3b  24497  minveclem4  24501  minveclem6  24503  ivthicc  24527  ovollb2lem  24557  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem2  24587  ovolicc2lem3  24588  ovolicc2lem4  24589  ovolicc2lem5  24590  ioombl1lem1  24627  dyadmaxlem  24666  volivth  24676  vitalilem2  24678  vitalilem4  24680  i1fima2  24748  itg2monolem1  24820  itgcnlem  24859  itgrevallem1  24864  itgreval  24866  itgle  24879  ibladd  24890  iblabslem  24897  itgspliticc  24906  itgsplitioo  24907  ditgcl  24927  ditgswap  24928  ditgsplitlem  24929  limcdif  24945  limcresi  24954  limcres  24955  limccnp  24960  limccnp2  24961  limcun  24964  dvlip  25062  dvlip2  25064  dveq0  25069  dvgt0lem1  25071  dvivthlem1  25077  dvcnvrelem1  25086  dvcnvre  25088  dvfsumlem2  25096  ftc1lem1  25104  ftc1lem2  25105  ftc1a  25106  ftc1lem4  25108  ftc2  25113  ftc2ditglem  25114  itgsubstlem  25117  ply1rem  25233  fta1glem2  25236  ig1pdvds  25246  plyrem  25370  fta1lem  25372  vieta1lem2  25376  aaliou3lem3  25409  pserulm  25486  psercnlem2  25488  psercnlem1  25489  psercn  25490  pserdvlem1  25491  pserdvlem2  25492  abelth2  25506  coseq00topi  25564  coseq0negpitopi  25565  cosordlem  25591  tanord1  25598  efif1olem1  25603  dvloglem  25708  efopnlem1  25716  logreclem  25817  relogbval  25827  nnlogbexp  25836  logbrec  25837  chordthmlem4  25890  quart1  25911  quartlem2  25913  quartlem3  25914  quart  25916  acosbnd  25955  atancj  25965  atanlogsublem  25970  atantan  25978  atanbndlem  25980  atans2  25986  dvatan  25990  atantayl  25992  divsqrtsumlem  26034  ftalem5  26131  basellem5  26139  ppisval  26158  chtleppi  26263  chpchtsum  26272  chpub  26273  mersenne  26280  perfectlem2  26283  dchrinv  26314  rplogsumlem2  26538  chpdifbndlem1  26606  pntibndlem2  26644  pntlema  26649  pntlemb  26650  pntlemg  26651  pntlemh  26652  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntlemp  26663  pntleml  26664  abvcxp  26668  ostth2lem2  26687  axtgcont1  26733  cgr3simp3  26787  legso  26864  hlln  26872  hltr  26875  btwnhl  26879  mirhl  26944  mirbtwnhl  26945  opphllem4  27015  opphl  27019  hlpasch  27021  cgracgr  27083  cgraswap  27085  cgrahl  27092  cgracol  27093  inagswap  27106  inagne3  27109  dfcgrg2  27128  umgrnloopv  27379  umgredgne  27418  usgrnloopvALT  27471  frusgrnn0  27841  cusgrm1rusgr  27852  upgrclwlkcompim  28050  2wlkdlem6  28197  2wlkond  28203  2trlond  28205  numclwwlk2lem1  28641  numclwlk2lem2f1o  28644  tncp  28741  grpolidinv  28764  nvs  28926  nvz  28932  nvtri  28933  sspn  28999  minvecolem2  29138  minvecolem4c  29142  minvecolem4  29143  minvecolem5  29144  minvecolem6  29145  adj1  30196  eliccelico  31000  elicoelioo  31001  prmdvdsbc  31032  pmtrto1cl  31268  cyc3evpm  31319  slmdvsdir  31371  slmd0vs  31379  nsgqusf1olem3  31502  prmidl  31517  prmidlc  31526  qsidomlem2  31531  mxidlmax  31539  locfinreflem  31692  cnre2csqlem  31762  sigaclci  32000  unelsiga  32002  insiga  32005  unelldsys  32026  ldsysgenld  32028  sigapildsys  32030  ldgenpisyslem1  32031  measvun  32077  cntmeas  32094  sibfima  32205  signstfveq0  32456  tg5segofs  32553  bnj1018g  32843  bnj1018  32844  pfxwlk  32985  revwlk  32986  spthcycl  32991  acycgrcycl  33009  subfacp1lem3  33044  subfacp1lem4  33045  subfacp1lem5  33046  sconnpht2  33100  sconnpi1  33101  txsconn  33103  resconn  33108  cvmcn  33124  cvmsuni  33131  cvmsdisj  33132  cvmshmeo  33133  cvmlift2lem8  33172  cvmlift2lem13  33177  cvmliftphtlem  33179  cvmliftpht  33180  cvmlift3lem6  33186  msrf  33404  elmsta  33410  mthmpps  33444  mclsppslem  33445  scutun12  33931  slerec  33940  cofcut2  34018  cofcutr  34019  cofcutrtime  34020  ivthALT  34451  relowlssretop  35461  ibladdnc  35761  iblabsnclem  35767  ftc2nc  35786  dvasin  35788  isbndx  35867  isbnd3  35869  prdsbnd  35878  heiborlem3  35898  iccbnd  35925  rngohomadd  36054  rngohommul  36055  idladdcl  36104  idllmulcl  36105  idlrmulcl  36106  maxidlmax  36128  pridlc  36156  eqvreltr  36647  lshpnelb  36925  lshpcmp  36929  oplecon3  37140  opnoncon  37149  hlcvl  37300  dochshpncl  39325  lclkrslem1  39478  lclkrslem2  39479  fzne2d  39917  sticksstones3  40032  metakunt8  40060  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt24  40076  metakunt25  40077  evlsval3  40195  flt4lem5f  40410  flt4lem7  40412  nna4b4nsq  40413  acongrep  40718  ntrneinex  41576  neicvgmex  41616  gneispace0nelrn  41639  cvgdvgrat  41820  binomcxplemdvbinom  41860  eliocre  42937  iccshift  42946  iccsuble  42947  icoiccdif  42952  mullimc  43047  limccog  43051  limciccioolb  43052  mullimcf  43054  limcperiod  43059  lptioo2  43062  lptioo1  43063  neglimc  43078  addlimc  43079  0ellimcdiv  43080  reclimc  43084  xlimmnfvlem1  43263  xlimpnfvlem1  43267  icccncfext  43318  cncfioobdlem  43327  ditgeqiooicc  43391  iblspltprt  43404  iblcncfioo  43409  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem11  43442  stoweidlem31  43462  stoweidlem36  43467  stoweidlem38  43469  stoweidlem62  43493  dirkercncflem1  43534  dirkercncflem4  43537  fourierdlem26  43564  fourierdlem32  43570  fourierdlem33  43571  fourierdlem37  43575  fourierdlem42  43580  fourierdlem54  43591  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem93  43630  fourierdlem101  43638  fourierdlem107  43644  fourierdlem109  43646  fourierdlem111  43648  salunicl  43747  saluncl  43748  hoidmv1lelem1  44019  hoidmv1lelem3  44021  hoidmvlelem1  44023  ovolval3  44075  iinhoiicclem  44101  smfpreimalt  44154  smfpreimaltf  44159  smfpreimale  44177  issmfgt  44179  smfpreimagt  44184  smfpreimage  44204  sigardiv  44264  sigarcol  44267  sharhght  44268  sigaradd  44269  cevathlem1  44270  cevathlem2  44271  cevath  44272  proththd  44954  perfectALTVlem2  45062