Theorem simp3 1026

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 1023	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl3  1029  simpr3  1032  simp3i  1035  simp3d  1038  simp13  1056  simp23  1059  simp33  1062  3anibar  1192  3ianorr  1346  intn3an3d  1395  stoic4a  1477  stoic4b  1478  mob2  2996  sotri2  5159  sotri3  5160  feq123  5499  resasplitss  5543  fresaunres2disj  5544  sefvex  5690  ftpg  5867  fsnunf  5883  fnfvima  5920  cocan1  5959  cocan2  5960  f1oiso2  5999  riotass  6032  moriotass  6033  ovmpox  6181  ovmpoga  6182  fvmpopr2d  6189  caovimo  6247  ofrval  6276  suppvalfn  6440  fvn0elsuppb  6451  dfsmo2  6517  tfr1onlembfn  6574  tfrcllembfn  6587  freccllem  6632  frecfcllem  6634  frecsuclem  6636  frecrdg  6638  nnsucsssuc  6724  f1oen2g  6993  f1dom2g  6994  xpdom3m  7084  mapxpen  7100  diffifi  7150  unfidisj  7181  undifdc  7183  imaf1fi  7192  ssfidc  7197  sbthlemi9  7234  ctssdc  7403  endjudisj  7516  djuassen  7523  xpdjuen  7524  mulcanenq  7696  ltanqg  7711  addnnnq0  7760  nnanq0  7769  prltlu  7798  distrprg  7899  ltexprlemm  7911  recexprlem1ssl  7944  recexprlem1ssu  7945  addsrpr  8056  mulsrpr  8057  mulasssrg  8069  recexgt0sr  8084  ltpsrprg  8114  axmulass  8184  axpre-ltadd  8197  ltxrlt  8335  subadd2  8473  addsubass  8479  nppcan  8491  nppcan3  8493  subcan2  8494  subsub2  8497  subsub4  8502  pnpcan  8508  pnncan  8510  subcan  8524  subdi  8654  ltadd1  8699  leadd1  8700  leadd2  8701  ltsubadd  8702  ltsubadd2  8703  lesubadd  8704  lesubadd2  8705  ltaddsub  8706  leaddsub  8708  lesub1  8726  lesub2  8727  ltsub1  8728  ltsub2  8729  ltaddsublt  8841  gt0add  8843  reapadd1  8866  remulext1  8869  remulext2  8870  apadd2  8879  mulext2  8883  mulap0r  8885  leltap  8895  ltap  8903  apsub1  8912  divap0b  8953  divmulasscomap  8966  divcanap5  8984  dmdcanap  8992  redivclap  9001  div2negap  9005  lt2msq1  9155  ltdiv2  9157  ofnegsub  9232  nndivtr  9275  difgtsumgt  9643  gtndiv  9669  eluzsub  9880  nn01to3  9945  qdivcl  9971  irrmul  9975  rpgecl  10011  divge1  10052  xaddass  10198  xltadd1  10205  ubioog  10243  ubioc1  10258  lbico1  10259  iccleub  10260  lbicc2  10313  ubicc2  10314  icoshftf1o  10320  fzen  10373  elfz1b  10420  uznfz  10433  elfzo0  10516  elfzo0z  10519  ubmelfzo  10541  fzonn0p1p1  10554  ubmelm1fzo  10567  zsupssdc  10594  qbtwnre  10612  flqwordi  10644  flltdivnn0lt  10660  ceiqle  10671  modqval  10682  modqvalr  10683  modqcl  10684  flqpmodeq  10685  modq0  10687  mulqmod0  10688  negqmod0  10689  modqge0  10690  modqlt  10691  modqdiffl  10693  modqdifz  10694  modqmulnn  10700  modqvalp1  10701  modqabs2  10716  modqmuladdnn0  10726  qnegmod  10727  addmodid  10730  modqeqmodmin  10752  modfzo0difsn  10753  addmodlteq  10756  frec2uzf1od  10764  expnegap0  10905  expgt1  10935  exprecap  10938  expaddzaplem  10940  expaddzap  10941  expmulzap  10943  mulbinom2  11014  expnbnd  11021  fihashss  11176  fimaxq  11187  seq3coll  11207  ccatw2s1leng  11319  ccat2s1fvwd  11328  swrdval  11333  swrdnd  11344  swrdlen2  11347  pfxn0  11373  ccatopth2  11402  s3cl  11471  s3fv0g  11476  s3fv1g  11477  s3fv2g  11478  shftfibg  11498  redivap  11552  imdivap  11559  cjdivap  11587  maxleast  11891  lemininf  11912  ltmininf  11913  bdtrilem  11917  bdtri  11918  xrmaxaddlem  11938  xrmaxadd  11939  xrmineqinf  11947  xrltmininf  11948  xrminltinf  11950  xrminadd  11953  climuni  11971  reccn2ap  11991  isumz  12068  fsumsplitsnun  12098  geoisum1c  12199  prodfap0  12224  prod1dc  12265  fprodabs  12295  cos12dec  12447  summodnegmod  12501  dvdsmultr2  12512  mulmoddvds  12542  divalglemeuneg  12602  gcdaddm  12673  gcdass  12704  mulgcd  12705  gcddiv  12708  nnminle  12724  lcmass  12775  mulgcddvds  12784  qredeq  12786  congr  12790  divgcdcoprmex  12792  cncongr1  12793  cncongr2  12794  prmexpb  12841  rpexp  12843  pythagtriplem1  12956  pythagtriplem6  12961  pythagtriplem7  12962  pythagtriplem12  12966  pythagtriplem13  12967  pythagtriplem15  12969  pythagtriplem19  12973  pcdiv  12993  dvdsprmpweqle  13028  sumhashdc  13038  pcbc  13042  4sqlem12  13093  4sqlem18  13099  unennn  13137  nninfdc  13193  fvsetsid  13235  ressressg  13277  rngmulrg  13340  imasaddvallemg  13517  qusaddvallemg  13535  mgmsscl  13563  plusfvalg  13565  ress0g  13645  imasmnd2  13654  imasmnd  13655  gsumfzz  13697  grpasscan2  13766  grpidrcan  13767  grpidlcan  13768  grpinvadd  13780  grppncan  13793  dfgrp3me  13802  grpsubpropd2  13807  pwsinvg  13814  imasgrp2  13816  imasgrp  13817  mhmmnd  13822  mulgnnsubcl  13840  mulgnn0subcl  13841  mulgsubcl  13842  mulgaddcomlem  13851  mulgaddcom  13852  mulgpropdg  13870  submmulg  13872  subgcl  13890  subgsubcl  13891  subgsub  13892  subgmulg  13894  nsgconj  13912  ghmsub  13957  ghmnsgima  13974  ghmeqker  13977  f1ghm0to0  13978  ablinvadd  14016  ablpncan2  14022  subgabl  14038  rngcl  14077  imasrng  14089  srgcl  14103  ringcl  14146  crngcom  14147  ringidss  14162  ringcom  14164  mulgass2  14191  imasring  14197  opprringbg  14213  unitmulcl  14247  unitmulclb  14248  dvrcl  14269  unitdvcl  14270  dvrcan1  14274  dvrcan3  14275  rhmmul  14298  subrngmcl  14343  subrgmcl  14367  subrgdv  14372  domneq0  14407  islmod  14426  scafvalg  14442  lmodcom  14468  lmodprop2d  14483  rmodislmodlem  14485  rmodislmod  14486  lsselg  14496  lssvnegcl  14511  lspss  14534  lspun  14537  lspsnvsi  14553  lsslsp  14564  sralmod  14585  lidlnegcl  14620  rspssp  14629  rnglidlrng  14633  qus2idrng  14660  zndvds  14784  psrbagaddclfi  14812  psrbagcon  14813  basgen  14932  2basgeng  14934  ntrss  14971  neiss  15002  opnneiss  15010  restco  15026  restabs  15027  cnprcl2k  15058  cnpf2  15059  lmconst  15068  cnpnei  15071  cnptoprest  15091  cnmpt2t  15145  psmetsym  15181  psmetge0  15183  xmetge0  15217  xmetsym  15220  blvalps  15240  blval  15241  ssblps  15277  ssbl  15278  blpnfctr  15291  xmssym  15321  bdxmet  15353  metcnp3  15363  dvfvalap  15533  dvid  15547  dvidre  15549  dvcnp2cntop  15551  elplyr  15592  ply1term  15595  plypow  15596  ptolemy  15676  rpcxpadd  15757  rpcxpsub  15760  rpmulcxp  15761  cxpmul  15764  rpcxple2  15770  rpcxplt2  15771  cxpcom  15790  rplogbval  15797  rplogbcl  15798  rplogbchbase  15802  rplogbreexp  15805  relogbexpap  15810  logbleb  15813  logblt  15814  rplogbcxp  15815  rpcxplogb  15816  relogbcxpbap  15817  sgmppw  15847  lgslem1  15860  lgsfvalg  15865  lgsval4  15880  lgsneg  15884  lgsne0  15898  lgsdinn0  15908  lgsquad  15940  funvtxvalg  16018  funiedgvalg  16019  upgrex  16085  uhgr2edg  16188  usgr2v1e2w  16228  subumgredg2en  16253  iedginwlk  16339  upgrwlkedg  16343  clwwlkccat  16383  clwwlknonex2  16421  eulerpathprum  16462  repiecele0  16797  repiecege0  16798  gfsumsn  16853