Theorem simp3 1030

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl3  1033  simpr3  1036  simp3i  1039  simp3d  1042  simp13  1060  simp23  1063  simp33  1066  3anibar  1196  3ianorr  1350  intn3an3d  1399  stoic4a  1481  stoic4b  1482  mob2  3006  ifprdc  3819  sotri2  5185  sotri3  5186  feq123  5525  resasplitss  5569  fresaunres2disj  5570  sefvex  5716  ftpg  5899  fsnunf  5915  fnfvima  5953  cocan1  5993  cocan2  5994  f1oiso2  6033  riotass  6068  moriotass  6069  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  ofrval  6313  suppvalfn  6481  fvn0elsuppb  6492  dfsmo2  6558  tfr1onlembfn  6615  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  nnsucsssuc  6765  f1oen2g  7041  f1dom2g  7042  xpdom3m  7132  mapxpen  7148  diffifi  7198  unfidisj  7229  undifdc  7231  imaf1fi  7240  ssfidc  7245  sbthlemi9  7282  fdcf1  7316  ctssdc  7453  endjudisj  7566  djuassen  7573  xpdjuen  7574  mulcanenq  7752  ltanqg  7767  addnnnq0  7816  nnanq0  7825  prltlu  7854  distrprg  7955  ltexprlemm  7967  recexprlem1ssl  8000  recexprlem1ssu  8001  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  recexgt0sr  8140  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  ltxrlt  8391  subadd2  8530  addsubass  8536  nppcan  8548  nppcan3  8550  subcan2  8551  subsub2  8554  subsub4  8559  pnpcan  8565  pnncan  8567  subcan  8581  subdi  8712  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltaddsublt  8900  gt0add  8902  reapadd1  8925  remulext1  8928  remulext2  8929  apadd2  8938  mulext2  8942  mulap0r  8944  leltap  8954  ltap  8962  apsub1  8971  divap0b  9014  divmulasscomap  9027  divcanap5  9045  dmdcanap  9053  redivclap  9062  div2negap  9066  lt2msq1  9216  ltdiv2  9218  ofnegsub  9293  indfval  9300  ind1  9301  nndivtr  9347  difgtsumgt  9716  zfidc  9725  gtndiv  9743  eluzsub  9954  nn01to3  10019  qdivcl  10045  irrmul  10049  rpgecl  10085  divge1  10126  xaddass  10273  xltadd1  10280  ubioog  10318  ubioc1  10333  lbico1  10334  iccleub  10335  lbicc2  10388  ubicc2  10389  icoshftf1o  10395  fzen  10449  elfz1b  10499  uznfz  10512  elfzo0  10595  elfzo0z  10598  ubmelfzo  10620  fzonn0p1p1  10633  ubmelm1fzo  10646  zsupssdc  10675  qbtwnre  10693  flqwordi  10725  flltdivnn0lt  10741  ceiqle  10752  modqval  10763  modqvalr  10764  modqcl  10765  flqpmodeq  10766  modq0  10768  mulqmod0  10769  negqmod0  10770  modqge0  10771  modqlt  10772  modqdiffl  10774  modqdifz  10775  modqmulnn  10781  modqvalp1  10782  modqabs2  10797  modqmuladdnn0  10807  qnegmod  10808  addmodid  10811  modqeqmodmin  10833  modfzo0difsn  10834  addmodlteq  10837  frec2uzf1od  10845  expnegap0  10986  expgt1  11016  exprecap  11019  expaddzaplem  11021  expaddzap  11022  expmulzap  11024  mulbinom2  11095  expnbnd  11103  fihashss  11259  fimaxq  11272  seq3coll  11296  ccatw2s1leng  11408  ccat2s1fvwd  11417  swrdval  11422  swrdnd  11433  swrdlen2  11436  pfxn0  11462  ccatopth2  11491  s3cl  11560  s3fv0g  11565  s3fv1g  11566  s3fv2g  11567  shftfibg  11587  redivap  11641  imdivap  11648  cjdivap  11677  maxleast  11981  lemininf  12002  ltmininf  12003  bdtrilem  12007  bdtri  12008  xrmaxaddlem  12028  xrmaxadd  12029  xrmineqinf  12037  xrltmininf  12038  xrminltinf  12040  xrminadd  12043  climuni  12061  reccn2ap  12081  isumz  12158  fsumsplitsnun  12188  geoisum1c  12289  prodfap0  12314  prod1dc  12355  fprodabs  12385  cos12dec  12537  summodnegmod  12591  dvdsmultr2  12602  mulmoddvds  12632  divalglemeuneg  12692  gcdaddm  12763  gcdass  12794  mulgcd  12795  gcddiv  12798  nnminle  12814  lcmass  12865  mulgcddvds  12874  qredeq  12876  congr  12880  divgcdcoprmex  12882  cncongr1  12883  cncongr2  12884  prmexpb  12931  rpexp  12933  pythagtriplem1  13046  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem12  13056  pythagtriplem13  13057  pythagtriplem15  13059  pythagtriplem19  13063  pcdiv  13083  dvdsprmpweqle  13118  sumhashdc  13128  pcbc  13132  4sqlem12  13183  4sqlem18  13189  ballotfilemsgt1  13256  ballotfilemfrcn0  13275  unennn  13290  nninfdc  13346  fvsetsid  13388  ressressg  13431  rngmulrg  13494  imasaddvallemg  13638  qusaddvallemg  13656  mgmsscl  13683  plusfvalg  13685  ress0g  13758  imasmnd2  13761  imasmnd  13762  grpasscan2  13871  grpidrcan  13872  grpidlcan  13873  grpinvadd  13885  grppncan  13898  dfgrp3me  13907  grpsubpropd2  13912  imasgrp2  13915  imasgrp  13916  mhmmnd  13921  mulgnnsubcl  13939  mulgnn0subcl  13940  mulgsubcl  13941  mulgaddcomlem  13950  mulgaddcom  13951  mulgpropdg  13969  submmulg  13971  subgcl  13989  subgsubcl  13990  subgsub  13991  subgmulg  13993  nsgconj  14011  ghmsub  14056  ghmnsgima  14073  ghmeqker  14076  f1ghm0to0  14077  ablinvadd  14116  ablpncan2  14122  subgabl  14138  gsumsncmn  14158  gsumconstcmn  14168  pwsinvg  14217  rngcl  14245  imasrng  14257  rng1zrlem  14260  srgcl  14276  ringcl  14319  crngcom  14320  ringidss  14336  ringcom  14338  mulgass2  14365  imasring  14371  opprringbg  14387  unitmulcl  14422  unitmulclb  14423  dvrcl  14444  unitdvcl  14445  dvrcan1  14449  dvrcan3  14450  rhmmul  14473  subrngmcl  14519  subrgmcl  14543  subrgdv  14548  domneq0  14583  islmod  14629  scafvalg  14646  lmodcom  14672  lmodprop2d  14687  rmodislmodlem  14689  rmodislmod  14690  lsselg  14700  lssvnegcl  14715  lspss  14738  lspun  14741  lspsnvsi  14757  lsslsp  14768  sralmod  14789  lidlnegcl  14824  rspssp  14833  rnglidlrng  14837  qus2idrng  14864  zndvds  14986  aspss  15021  asclmul1  15031  asclmul2  15032  ascldimul  15033  asclinvg  15034  asclmulg  15046  psrbagaddclfi  15063  psrbagcon  15064  basgen  15183  2basgeng  15185  ntrss  15222  neiss  15253  opnneiss  15261  restco  15277  restabs  15278  cnprcl2k  15309  cnpf2  15310  lmconst  15319  cnpnei  15322  cnptoprest  15342  cnmpt2t  15396  psmetsym  15432  psmetge0  15434  xmetge0  15468  xmetsym  15471  blvalps  15491  blval  15492  ssblps  15528  ssbl  15529  blpnfctr  15542  xmssym  15572  bdxmet  15604  metcnp3  15614  dvfvalap  15784  dvid  15798  dvidre  15800  dvcnp2cntop  15802  elplyr  15843  ply1term  15846  plypow  15847  ptolemy  15928  logfac  16001  rpcxpadd  16013  rpcxpsub  16016  rpmulcxp  16017  cxpmul  16020  rpcxple2  16026  rpcxplt2  16027  cxpcom  16046  rplogbval  16053  rplogbcl  16054  rplogbchbase  16058  rplogbreexp  16061  relogbexpap  16066  logbleb  16069  logblt  16070  rplogbcxp  16071  rpcxplogb  16072  relogbcxpbap  16073  sgmppw  16112  bcmono  16124  lgslem1  16131  lgsfvalg  16136  lgsval4  16151  lgsneg  16155  lgsne0  16169  lgsdinn0  16179  lgsquad  16211  funvtxvalg  16289  funiedgvalg  16290  upgrex  16356  uhgr2edg  16459  usgr2v1e2w  16499  subumgredg2en  16524  iedginwlk  16610  upgrwlkedg  16614  clwwlkccat  16654  clwwlknonex2  16692  eulerpathprum  16733  dichmul0or  16772  repiecele0  17087  repiecege0  17088