Theorem simp3 1025

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simpl3  1028  simpr3  1031  simp3i  1034  simp3d  1037  simp13  1055  simp23  1058  simp33  1061  3anibar  1191  3ianorr  1345  intn3an3d  1394  stoic4a  1476  stoic4b  1477  mob2  2985  sotri2  5136  sotri3  5137  feq123  5476  resasplitss  5518  sefvex  5663  ftpg  5841  fsnunf  5857  fnfvima  5894  cocan1  5933  cocan2  5934  f1oiso2  5973  riotass  6006  moriotass  6007  ovmpox  6155  ovmpoga  6156  fvmpopr2d  6163  caovimo  6221  ofrval  6251  dfsmo2  6458  tfr1onlembfn  6515  tfrcllembfn  6528  freccllem  6573  frecfcllem  6575  frecsuclem  6577  frecrdg  6579  nnsucsssuc  6665  f1oen2g  6933  f1dom2g  6934  xpdom3m  7023  mapxpen  7039  diffifi  7088  unfidisj  7119  undifdc  7121  imaf1fi  7130  ssfidc  7135  sbthlemi9  7169  ctssdc  7317  endjudisj  7430  djuassen  7437  xpdjuen  7438  mulcanenq  7610  ltanqg  7625  addnnnq0  7674  nnanq0  7683  prltlu  7712  distrprg  7813  ltexprlemm  7825  recexprlem1ssl  7858  recexprlem1ssu  7859  addsrpr  7970  mulsrpr  7971  mulasssrg  7983  recexgt0sr  7998  ltpsrprg  8028  axmulass  8098  axpre-ltadd  8111  ltxrlt  8250  subadd2  8388  addsubass  8394  nppcan  8406  nppcan3  8408  subcan2  8409  subsub2  8412  subsub4  8417  pnpcan  8423  pnncan  8425  subcan  8439  subdi  8569  ltadd1  8614  leadd1  8615  leadd2  8616  ltsubadd  8617  ltsubadd2  8618  lesubadd  8619  lesubadd2  8620  ltaddsub  8621  leaddsub  8623  lesub1  8641  lesub2  8642  ltsub1  8643  ltsub2  8644  ltaddsublt  8756  gt0add  8758  reapadd1  8781  remulext1  8784  remulext2  8785  apadd2  8794  mulext2  8798  mulap0r  8800  leltap  8810  ltap  8818  apsub1  8827  divap0b  8868  divmulasscomap  8881  divcanap5  8899  dmdcanap  8907  redivclap  8916  div2negap  8920  lt2msq1  9070  ltdiv2  9072  ofnegsub  9147  nndivtr  9190  difgtsumgt  9554  gtndiv  9580  eluzsub  9791  nn01to3  9856  qdivcl  9882  irrmul  9886  rpgecl  9922  divge1  9963  xaddass  10109  xltadd1  10116  ubioog  10154  ubioc1  10169  lbico1  10170  iccleub  10171  lbicc2  10224  ubicc2  10225  icoshftf1o  10231  fzen  10283  elfz1b  10330  uznfz  10343  elfzo0  10426  elfzo0z  10429  ubmelfzo  10451  fzonn0p1p1  10464  ubmelm1fzo  10477  zsupssdc  10504  qbtwnre  10522  flqwordi  10554  flltdivnn0lt  10570  ceiqle  10581  modqval  10592  modqvalr  10593  modqcl  10594  flqpmodeq  10595  modq0  10597  mulqmod0  10598  negqmod0  10599  modqge0  10600  modqlt  10601  modqdiffl  10603  modqdifz  10604  modqmulnn  10610  modqvalp1  10611  modqabs2  10626  modqmuladdnn0  10636  qnegmod  10637  addmodid  10640  modqeqmodmin  10662  modfzo0difsn  10663  addmodlteq  10666  frec2uzf1od  10674  expnegap0  10815  expgt1  10845  exprecap  10848  expaddzaplem  10850  expaddzap  10851  expmulzap  10853  mulbinom2  10924  expnbnd  10931  fihashss  11086  fimaxq  11097  seq3coll  11112  ccatw2s1leng  11224  ccat2s1fvwd  11233  swrdval  11238  swrdnd  11249  swrdlen2  11252  pfxn0  11278  ccatopth2  11307  s3cl  11376  s3fv0g  11381  s3fv1g  11382  s3fv2g  11383  shftfibg  11403  redivap  11457  imdivap  11464  cjdivap  11492  maxleast  11796  lemininf  11817  ltmininf  11818  bdtrilem  11822  bdtri  11823  xrmaxaddlem  11843  xrmaxadd  11844  xrmineqinf  11852  xrltmininf  11853  xrminltinf  11855  xrminadd  11858  climuni  11876  reccn2ap  11896  isumz  11973  fsumsplitsnun  12003  geoisum1c  12104  prodfap0  12129  prod1dc  12170  fprodabs  12200  cos12dec  12352  summodnegmod  12406  dvdsmultr2  12417  mulmoddvds  12447  divalglemeuneg  12507  gcdaddm  12578  gcdass  12609  mulgcd  12610  gcddiv  12613  nnminle  12629  lcmass  12680  mulgcddvds  12689  qredeq  12691  congr  12695  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  prmexpb  12746  rpexp  12748  pythagtriplem1  12861  pythagtriplem6  12866  pythagtriplem7  12867  pythagtriplem12  12871  pythagtriplem13  12872  pythagtriplem15  12874  pythagtriplem19  12878  pcdiv  12898  dvdsprmpweqle  12933  sumhashdc  12943  pcbc  12947  4sqlem12  12998  4sqlem18  13004  unennn  13041  nninfdc  13097  fvsetsid  13139  ressressg  13181  rngmulrg  13244  imasaddvallemg  13421  qusaddvallemg  13439  mgmsscl  13467  plusfvalg  13469  ress0g  13549  imasmnd2  13558  imasmnd  13559  gsumfzz  13601  grpasscan2  13670  grpidrcan  13671  grpidlcan  13672  grpinvadd  13684  grppncan  13697  dfgrp3me  13706  grpsubpropd2  13711  pwsinvg  13718  imasgrp2  13720  imasgrp  13721  mhmmnd  13726  mulgnnsubcl  13744  mulgnn0subcl  13745  mulgsubcl  13746  mulgaddcomlem  13755  mulgaddcom  13756  mulgpropdg  13774  submmulg  13776  subgcl  13794  subgsubcl  13795  subgsub  13796  subgmulg  13798  nsgconj  13816  ghmsub  13861  ghmnsgima  13878  ghmeqker  13881  f1ghm0to0  13882  ablinvadd  13920  ablpncan2  13926  subgabl  13942  rngcl  13981  imasrng  13993  srgcl  14007  ringcl  14050  crngcom  14051  ringidss  14066  ringcom  14068  mulgass2  14095  imasring  14101  opprringbg  14117  unitmulcl  14151  unitmulclb  14152  dvrcl  14173  unitdvcl  14174  dvrcan1  14178  dvrcan3  14179  rhmmul  14202  subrngmcl  14247  subrgmcl  14271  subrgdv  14276  domneq0  14310  islmod  14329  scafvalg  14345  lmodcom  14371  lmodprop2d  14386  rmodislmodlem  14388  rmodislmod  14389  lsselg  14399  lssvnegcl  14414  lspss  14437  lspun  14440  lspsnvsi  14456  lsslsp  14467  sralmod  14488  lidlnegcl  14523  rspssp  14532  rnglidlrng  14536  qus2idrng  14563  zndvds  14687  psrbagcon  14714  basgen  14833  2basgeng  14835  ntrss  14872  neiss  14903  opnneiss  14911  restco  14927  restabs  14928  cnprcl2k  14959  cnpf2  14960  lmconst  14969  cnpnei  14972  cnptoprest  14992  cnmpt2t  15046  psmetsym  15082  psmetge0  15084  xmetge0  15118  xmetsym  15121  blvalps  15141  blval  15142  ssblps  15178  ssbl  15179  blpnfctr  15192  xmssym  15222  bdxmet  15254  metcnp3  15264  dvfvalap  15434  dvid  15448  dvidre  15450  dvcnp2cntop  15452  elplyr  15493  ply1term  15496  plypow  15497  ptolemy  15577  rpcxpadd  15658  rpcxpsub  15661  rpmulcxp  15662  cxpmul  15665  rpcxple2  15671  rpcxplt2  15672  cxpcom  15691  rplogbval  15698  rplogbcl  15699  rplogbchbase  15703  rplogbreexp  15706  relogbexpap  15711  logbleb  15714  logblt  15715  rplogbcxp  15716  rpcxplogb  15717  relogbcxpbap  15718  sgmppw  15745  lgslem1  15758  lgsfvalg  15763  lgsval4  15778  lgsneg  15782  lgsne0  15796  lgsdinn0  15806  lgsquad  15838  funvtxvalg  15916  funiedgvalg  15917  upgrex  15983  uhgr2edg  16086  usgr2v1e2w  16126  subumgredg2en  16151  iedginwlk  16237  upgrwlkedg  16241  clwwlkccat  16281  clwwlknonex2  16319  eulerpathprum  16360  repiecele0  16697  repiecege0  16698  gfsumsn  16753