Theorem simp3 1004

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

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  simpl3  1007  simpr3  1010  simp3i  1013  simp3d  1016  simp13  1034  simp23  1037  simp33  1040  3anibar  1170  3ianorr  1324  intn3an3d  1372  stoic4a  1454  stoic4b  1455  mob2  2963  sotri2  5102  sotri3  5103  feq123  5441  resasplitss  5481  sefvex  5624  ftpg  5796  fsnunf  5812  fnfvima  5847  cocan1  5884  cocan2  5885  f1oiso2  5924  riotass  5957  moriotass  5958  ovmpox  6104  ovmpoga  6105  fvmpopr2d  6112  caovimo  6170  ofrval  6199  dfsmo2  6403  tfr1onlembfn  6460  tfrcllembfn  6473  freccllem  6518  frecfcllem  6520  frecsuclem  6522  frecrdg  6524  nnsucsssuc  6608  f1oen2g  6876  f1dom2g  6877  xpdom3m  6961  mapxpen  6977  diffifi  7024  unfidisj  7052  undifdc  7054  ssfidc  7067  sbthlemi9  7100  ctssdc  7248  endjudisj  7360  djuassen  7367  xpdjuen  7368  mulcanenq  7540  ltanqg  7555  addnnnq0  7604  nnanq0  7613  prltlu  7642  distrprg  7743  ltexprlemm  7755  recexprlem1ssl  7788  recexprlem1ssu  7789  addsrpr  7900  mulsrpr  7901  mulasssrg  7913  recexgt0sr  7928  ltpsrprg  7958  axmulass  8028  axpre-ltadd  8041  ltxrlt  8180  subadd2  8318  addsubass  8324  nppcan  8336  nppcan3  8338  subcan2  8339  subsub2  8342  subsub4  8347  pnpcan  8353  pnncan  8355  subcan  8369  subdi  8499  ltadd1  8544  leadd1  8545  leadd2  8546  ltsubadd  8547  ltsubadd2  8548  lesubadd  8549  lesubadd2  8550  ltaddsub  8551  leaddsub  8553  lesub1  8571  lesub2  8572  ltsub1  8573  ltsub2  8574  ltaddsublt  8686  gt0add  8688  reapadd1  8711  remulext1  8714  remulext2  8715  apadd2  8724  mulext2  8728  mulap0r  8730  leltap  8740  ltap  8748  apsub1  8757  divap0b  8798  divmulasscomap  8811  divcanap5  8829  dmdcanap  8837  redivclap  8846  div2negap  8850  lt2msq1  9000  ltdiv2  9002  ofnegsub  9077  nndivtr  9120  difgtsumgt  9484  gtndiv  9510  eluzsub  9720  nn01to3  9780  qdivcl  9806  irrmul  9810  rpgecl  9846  divge1  9887  xaddass  10033  xltadd1  10040  ubioog  10078  ubioc1  10093  lbico1  10094  iccleub  10095  lbicc2  10148  ubicc2  10149  icoshftf1o  10155  fzen  10207  elfz1b  10254  uznfz  10267  elfzo0  10350  elfzo0z  10352  ubmelfzo  10373  fzonn0p1p1  10386  ubmelm1fzo  10399  zsupssdc  10425  qbtwnre  10443  flqwordi  10475  flltdivnn0lt  10491  ceiqle  10502  modqval  10513  modqvalr  10514  modqcl  10515  flqpmodeq  10516  modq0  10518  mulqmod0  10519  negqmod0  10520  modqge0  10521  modqlt  10522  modqdiffl  10524  modqdifz  10525  modqmulnn  10531  modqvalp1  10532  modqabs2  10547  modqmuladdnn0  10557  qnegmod  10558  addmodid  10561  modqeqmodmin  10583  modfzo0difsn  10584  addmodlteq  10587  frec2uzf1od  10595  expnegap0  10736  expgt1  10766  exprecap  10769  expaddzaplem  10771  expaddzap  10772  expmulzap  10774  mulbinom2  10845  expnbnd  10852  fihashss  11005  fimaxq  11016  seq3coll  11031  swrdval  11146  swrdnd  11157  swrdlen2  11160  pfxn0  11186  ccatopth2  11215  s3cl  11284  s3fv0g  11289  s3fv1g  11290  shftfibg  11297  redivap  11351  imdivap  11358  cjdivap  11386  maxleast  11690  lemininf  11711  ltmininf  11712  bdtrilem  11716  bdtri  11717  xrmaxaddlem  11737  xrmaxadd  11738  xrmineqinf  11746  xrltmininf  11747  xrminltinf  11749  xrminadd  11752  climuni  11770  reccn2ap  11790  isumz  11866  fsumsplitsnun  11896  geoisum1c  11997  prodfap0  12022  prod1dc  12063  fprodabs  12093  cos12dec  12245  summodnegmod  12299  dvdsmultr2  12310  mulmoddvds  12340  divalglemeuneg  12400  gcdaddm  12471  gcdass  12502  mulgcd  12503  gcddiv  12506  nnminle  12522  lcmass  12573  mulgcddvds  12582  qredeq  12584  congr  12588  divgcdcoprmex  12590  cncongr1  12591  cncongr2  12592  prmexpb  12639  rpexp  12641  pythagtriplem1  12754  pythagtriplem6  12759  pythagtriplem7  12760  pythagtriplem12  12764  pythagtriplem13  12765  pythagtriplem15  12767  pythagtriplem19  12771  pcdiv  12791  dvdsprmpweqle  12826  sumhashdc  12836  pcbc  12840  4sqlem12  12891  4sqlem18  12897  unennn  12934  nninfdc  12990  fvsetsid  13032  ressressg  13074  rngmulrg  13137  imasaddvallemg  13314  qusaddvallemg  13332  mgmsscl  13360  plusfvalg  13362  ress0g  13442  imasmnd2  13451  imasmnd  13452  gsumfzz  13494  grpasscan2  13563  grpidrcan  13564  grpidlcan  13565  grpinvadd  13577  grppncan  13590  dfgrp3me  13599  grpsubpropd2  13604  pwsinvg  13611  imasgrp2  13613  imasgrp  13614  mhmmnd  13619  mulgnnsubcl  13637  mulgnn0subcl  13638  mulgsubcl  13639  mulgaddcomlem  13648  mulgaddcom  13649  mulgpropdg  13667  submmulg  13669  subgcl  13687  subgsubcl  13688  subgsub  13689  subgmulg  13691  nsgconj  13709  ghmsub  13754  ghmnsgima  13771  ghmeqker  13774  f1ghm0to0  13775  ablinvadd  13813  ablpncan2  13819  subgabl  13835  rngcl  13873  imasrng  13885  srgcl  13899  ringcl  13942  crngcom  13943  ringidss  13958  ringcom  13960  mulgass2  13987  imasring  13993  opprringbg  14009  unitmulcl  14042  unitmulclb  14043  dvrcl  14064  unitdvcl  14065  dvrcan1  14069  dvrcan3  14070  rhmmul  14093  subrngmcl  14138  subrgmcl  14162  subrgdv  14167  domneq0  14201  islmod  14220  scafvalg  14236  lmodcom  14262  lmodprop2d  14277  rmodislmodlem  14279  rmodislmod  14280  lsselg  14290  lssvnegcl  14305  lspss  14328  lspun  14331  lspsnvsi  14347  lsslsp  14358  sralmod  14379  lidlnegcl  14414  rspssp  14423  rnglidlrng  14427  qus2idrng  14454  zndvds  14578  basgen  14719  2basgeng  14721  ntrss  14758  neiss  14789  opnneiss  14797  restco  14813  restabs  14814  cnprcl2k  14845  cnpf2  14846  lmconst  14855  cnpnei  14858  cnptoprest  14878  cnmpt2t  14932  psmetsym  14968  psmetge0  14970  xmetge0  15004  xmetsym  15007  blvalps  15027  blval  15028  ssblps  15064  ssbl  15065  blpnfctr  15078  xmssym  15108  bdxmet  15140  metcnp3  15150  dvfvalap  15320  dvid  15334  dvidre  15336  dvcnp2cntop  15338  elplyr  15379  ply1term  15382  plypow  15383  ptolemy  15463  rpcxpadd  15544  rpcxpsub  15547  rpmulcxp  15548  cxpmul  15551  rpcxple2  15557  rpcxplt2  15558  cxpcom  15577  rplogbval  15584  rplogbcl  15585  rplogbchbase  15589  rplogbreexp  15592  relogbexpap  15597  logbleb  15600  logblt  15601  rplogbcxp  15602  rpcxplogb  15603  relogbcxpbap  15604  sgmppw  15631  lgslem1  15644  lgsfvalg  15649  lgsval4  15664  lgsneg  15668  lgsne0  15682  lgsdinn0  15692  lgsquad  15724  funvtxvalg  15802  funiedgvalg  15803  upgrex  15868  uhgr2edg  15969