Theorem simp3 1023

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 1020	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl3  1026  simpr3  1029  simp3i  1032  simp3d  1035  simp13  1053  simp23  1056  simp33  1059  3anibar  1189  3ianorr  1343  intn3an3d  1392  stoic4a  1474  stoic4b  1475  mob2  2983  sotri2  5129  sotri3  5130  feq123  5468  resasplitss  5510  sefvex  5653  ftpg  5830  fsnunf  5846  fnfvima  5881  cocan1  5920  cocan2  5921  f1oiso2  5960  riotass  5993  moriotass  5994  ovmpox  6142  ovmpoga  6143  fvmpopr2d  6150  caovimo  6208  ofrval  6238  dfsmo2  6444  tfr1onlembfn  6501  tfrcllembfn  6514  freccllem  6559  frecfcllem  6561  frecsuclem  6563  frecrdg  6565  nnsucsssuc  6651  f1oen2g  6919  f1dom2g  6920  xpdom3m  7006  mapxpen  7022  diffifi  7069  unfidisj  7100  undifdc  7102  ssfidc  7115  sbthlemi9  7148  ctssdc  7296  endjudisj  7408  djuassen  7415  xpdjuen  7416  mulcanenq  7588  ltanqg  7603  addnnnq0  7652  nnanq0  7661  prltlu  7690  distrprg  7791  ltexprlemm  7803  recexprlem1ssl  7836  recexprlem1ssu  7837  addsrpr  7948  mulsrpr  7949  mulasssrg  7961  recexgt0sr  7976  ltpsrprg  8006  axmulass  8076  axpre-ltadd  8089  ltxrlt  8228  subadd2  8366  addsubass  8372  nppcan  8384  nppcan3  8386  subcan2  8387  subsub2  8390  subsub4  8395  pnpcan  8401  pnncan  8403  subcan  8417  subdi  8547  ltadd1  8592  leadd1  8593  leadd2  8594  ltsubadd  8595  ltsubadd2  8596  lesubadd  8597  lesubadd2  8598  ltaddsub  8599  leaddsub  8601  lesub1  8619  lesub2  8620  ltsub1  8621  ltsub2  8622  ltaddsublt  8734  gt0add  8736  reapadd1  8759  remulext1  8762  remulext2  8763  apadd2  8772  mulext2  8776  mulap0r  8778  leltap  8788  ltap  8796  apsub1  8805  divap0b  8846  divmulasscomap  8859  divcanap5  8877  dmdcanap  8885  redivclap  8894  div2negap  8898  lt2msq1  9048  ltdiv2  9050  ofnegsub  9125  nndivtr  9168  difgtsumgt  9532  gtndiv  9558  eluzsub  9769  nn01to3  9829  qdivcl  9855  irrmul  9859  rpgecl  9895  divge1  9936  xaddass  10082  xltadd1  10089  ubioog  10127  ubioc1  10142  lbico1  10143  iccleub  10144  lbicc2  10197  ubicc2  10198  icoshftf1o  10204  fzen  10256  elfz1b  10303  uznfz  10316  elfzo0  10399  elfzo0z  10401  ubmelfzo  10423  fzonn0p1p1  10436  ubmelm1fzo  10449  zsupssdc  10475  qbtwnre  10493  flqwordi  10525  flltdivnn0lt  10541  ceiqle  10552  modqval  10563  modqvalr  10564  modqcl  10565  flqpmodeq  10566  modq0  10568  mulqmod0  10569  negqmod0  10570  modqge0  10571  modqlt  10572  modqdiffl  10574  modqdifz  10575  modqmulnn  10581  modqvalp1  10582  modqabs2  10597  modqmuladdnn0  10607  qnegmod  10608  addmodid  10611  modqeqmodmin  10633  modfzo0difsn  10634  addmodlteq  10637  frec2uzf1od  10645  expnegap0  10786  expgt1  10816  exprecap  10819  expaddzaplem  10821  expaddzap  10822  expmulzap  10824  mulbinom2  10895  expnbnd  10902  fihashss  11056  fimaxq  11067  seq3coll  11082  swrdval  11201  swrdnd  11212  swrdlen2  11215  pfxn0  11241  ccatopth2  11270  s3cl  11339  s3fv0g  11344  s3fv1g  11345  shftfibg  11352  redivap  11406  imdivap  11413  cjdivap  11441  maxleast  11745  lemininf  11766  ltmininf  11767  bdtrilem  11771  bdtri  11772  xrmaxaddlem  11792  xrmaxadd  11793  xrmineqinf  11801  xrltmininf  11802  xrminltinf  11804  xrminadd  11807  climuni  11825  reccn2ap  11845  isumz  11921  fsumsplitsnun  11951  geoisum1c  12052  prodfap0  12077  prod1dc  12118  fprodabs  12148  cos12dec  12300  summodnegmod  12354  dvdsmultr2  12365  mulmoddvds  12395  divalglemeuneg  12455  gcdaddm  12526  gcdass  12557  mulgcd  12558  gcddiv  12561  nnminle  12577  lcmass  12628  mulgcddvds  12637  qredeq  12639  congr  12643  divgcdcoprmex  12645  cncongr1  12646  cncongr2  12647  prmexpb  12694  rpexp  12696  pythagtriplem1  12809  pythagtriplem6  12814  pythagtriplem7  12815  pythagtriplem12  12819  pythagtriplem13  12820  pythagtriplem15  12822  pythagtriplem19  12826  pcdiv  12846  dvdsprmpweqle  12881  sumhashdc  12891  pcbc  12895  4sqlem12  12946  4sqlem18  12952  unennn  12989  nninfdc  13045  fvsetsid  13087  ressressg  13129  rngmulrg  13192  imasaddvallemg  13369  qusaddvallemg  13387  mgmsscl  13415  plusfvalg  13417  ress0g  13497  imasmnd2  13506  imasmnd  13507  gsumfzz  13549  grpasscan2  13618  grpidrcan  13619  grpidlcan  13620  grpinvadd  13632  grppncan  13645  dfgrp3me  13654  grpsubpropd2  13659  pwsinvg  13666  imasgrp2  13668  imasgrp  13669  mhmmnd  13674  mulgnnsubcl  13692  mulgnn0subcl  13693  mulgsubcl  13694  mulgaddcomlem  13703  mulgaddcom  13704  mulgpropdg  13722  submmulg  13724  subgcl  13742  subgsubcl  13743  subgsub  13744  subgmulg  13746  nsgconj  13764  ghmsub  13809  ghmnsgima  13826  ghmeqker  13829  f1ghm0to0  13830  ablinvadd  13868  ablpncan2  13874  subgabl  13890  rngcl  13928  imasrng  13940  srgcl  13954  ringcl  13997  crngcom  13998  ringidss  14013  ringcom  14015  mulgass2  14042  imasring  14048  opprringbg  14064  unitmulcl  14098  unitmulclb  14099  dvrcl  14120  unitdvcl  14121  dvrcan1  14125  dvrcan3  14126  rhmmul  14149  subrngmcl  14194  subrgmcl  14218  subrgdv  14223  domneq0  14257  islmod  14276  scafvalg  14292  lmodcom  14318  lmodprop2d  14333  rmodislmodlem  14335  rmodislmod  14336  lsselg  14346  lssvnegcl  14361  lspss  14384  lspun  14387  lspsnvsi  14403  lsslsp  14414  sralmod  14435  lidlnegcl  14470  rspssp  14479  rnglidlrng  14483  qus2idrng  14510  zndvds  14634  basgen  14775  2basgeng  14777  ntrss  14814  neiss  14845  opnneiss  14853  restco  14869  restabs  14870  cnprcl2k  14901  cnpf2  14902  lmconst  14911  cnpnei  14914  cnptoprest  14934  cnmpt2t  14988  psmetsym  15024  psmetge0  15026  xmetge0  15060  xmetsym  15063  blvalps  15083  blval  15084  ssblps  15120  ssbl  15121  blpnfctr  15134  xmssym  15164  bdxmet  15196  metcnp3  15206  dvfvalap  15376  dvid  15390  dvidre  15392  dvcnp2cntop  15394  elplyr  15435  ply1term  15438  plypow  15439  ptolemy  15519  rpcxpadd  15600  rpcxpsub  15603  rpmulcxp  15604  cxpmul  15607  rpcxple2  15613  rpcxplt2  15614  cxpcom  15633  rplogbval  15640  rplogbcl  15641  rplogbchbase  15645  rplogbreexp  15648  relogbexpap  15653  logbleb  15656  logblt  15657  rplogbcxp  15658  rpcxplogb  15659  relogbcxpbap  15660  sgmppw  15687  lgslem1  15700  lgsfvalg  15705  lgsval4  15720  lgsneg  15724  lgsne0  15738  lgsdinn0  15748  lgsquad  15780  funvtxvalg  15858  funiedgvalg  15859  upgrex  15924  uhgr2edg  16025  usgr2v1e2w  16065  iedginwlk  16129  upgrwlkedg  16133  clwwlkccat  16170