Theorem simp1 1028

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

Assertion

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

Proof of Theorem simp1

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simpld 112	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

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

This theorem is used by:  simpl1  1031  simpr1  1034  simp1i  1037  simp1d  1040  simp11  1058  simp21  1061  simp31  1064  syld3an3  1323  3ianorr  1350  intn3an1d  1397  stoic4a  1481  stoic4b  1482  rsp2e  2601  ifnetruedc  3684  issod  4466  elirr  4690  sotri2  5188  sotri3  5189  funtpg  5435  funimaexglem  5467  feq123  5528  ftpg  5902  fsnunf  5918  foco2  5962  fcofo  5993  f1oiso2  6036  riotass  6071  ovmpox  6220  ovmpoga  6221  caovimo  6286  ofeq  6308  ofrval  6317  fvn0elsuppb  6496  tfr1onlembxssdm  6618  tfrcllembxssdm  6631  frecsuclem  6681  frecrdg  6683  mapm  6974  domssr  7069  mapxpen  7153  diffifi  7203  unsnfidcex  7232  unsnfidcel  7233  unfidisj  7234  undifdc  7236  ssfidc  7250  iunfidisj  7265  fissfi  7268  sbthlemi9  7288  elfir  7313  fdcf1  7322  djuassen  7580  dftap2  7624  mulcanenq  7759  ltanqg  7774  addnnnq0  7823  distrlem4prl  7958  distrlem4pru  7959  distrprg  7962  aptipr  8015  addsrpr  8119  mulsrpr  8120  mulasssrg  8132  ltpsrprg  8177  axmulass  8247  axpre-ltadd  8260  mul31  8465  addsubass  8544  subcan2  8559  subsub2  8562  subsub4  8567  npncan3  8572  pnpcan  8573  pnncan  8575  subcan  8589  subdi  8720  ltadd1  8765  leadd1  8766  leadd2  8767  ltsubadd  8768  lesubadd  8770  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  ltaddsublt  8908  gt0add  8910  apreap  8924  lemul1  8930  reapmul1lem  8931  reapmul1  8932  reapadd1  8933  remulext1  8936  remulext2  8937  apadd2  8946  mulext2  8950  mulap0r  8952  leltap  8962  ltap  8970  apsub1  8979  recexaplem2  8989  mulcanap  9002  mulcanap2  9003  divvalap  9013  divcanap2  9019  diveqap0  9021  divrecap  9027  divrecap2  9028  divdirap  9036  divcanap3  9037  div11ap  9039  muldivdirap  9046  divcanap5  9053  redivclap  9070  div2negap  9074  apmul1  9127  apmul2  9128  div2subap  9176  ltdiv1  9207  ltmuldiv  9213  lemuldiv  9220  lt2msq1  9224  ltdiv23  9231  lediv23  9232  squeeze0  9243  ofsubeq0  9301  ofnegsub  9302  difgtsumgt  9726  zfidc  9735  gtndiv  9753  eluz2  9944  eluzsub  9969  peano2uz  10000  nn01to3  10034  divge1  10142  ledivge1le  10145  addlelt  10187  xaddass  10289  xleadd1  10295  xltadd1  10296  ixxssixx  10322  lbico1  10350  lbicc2  10404  icoshftf1o  10411  fzen  10465  fzrev3  10512  fzrevral2  10531  nelfzo  10577  elfzo0  10611  elfzo0z  10614  fzosplitprm1  10671  qbtwnre  10709  flqwordi  10745  flqword2  10746  adddivflid  10749  flltdivnn0lt  10761  modqcl  10785  mulqmod0  10789  modqmulnn  10801  modqabs2  10817  addmodid  10831  modifeq2int  10845  modqeqmodmin  10853  seqeq2  10910  seqeq3  10911  seq1g  10922  seqp1g  10925  exp3val  11000  expnegap0  11006  expgt1  11036  exprecap  11039  leexp2a  11051  expubnd  11055  sqdivap  11062  expnbnd  11123  mulsubdivbinom2ap  11172  bccmpl  11215  fihashss  11280  leisorel  11312  ccatass  11399  ccats1val2  11431  swrdval  11443  swrdval2  11446  swrdlen2  11457  swrdfv2  11458  pfxfv  11479  pfxn0  11483  pfxnd  11484  swrdswrd  11500  pfxswrd  11501  pfxpfx  11503  ccats1pfxeqbi  11537  s3cl  11581  s3fv0g  11586  s3fv1g  11587  s3fv2g  11588  shftfibg  11608  mulreap  11652  abssubne0  11881  maxleast  12003  lemininf  12025  ltmininf  12026  xrmaxltsup  12050  xrmaxaddlem  12052  xrmaxadd  12053  xrmineqinf  12061  xrltmininf  12062  xrminltinf  12064  xrminadd  12067  climuni  12085  reccn2ap  12105  isumz  12182  fsumsplitsnun  12212  geoisum1c  12313  prod1dc  12379  efltim  12491  dvdscmulr  12613  dvdsmulcr  12614  summodnegmod  12615  modmulconst  12616  dvdsmultr2  12626  dvdsexp  12654  mulmoddvds  12656  modremain  12722  divgcdz  12774  gcdaddm  12787  dvdsgcdb  12816  gcdass  12818  mulgcd  12819  gcddiv  12822  rplpwr  12830  uzwodc  12840  lcmdvdsb  12888  lcmass  12889  mulgcddvds  12898  qredeq  12900  qredeu  12901  rpmul  12902  divgcdcoprmex  12906  cncongr1  12907  rpexp  12958  rpexp12i  12960  odzcllem  13051  odzdvds  13054  odzphi  13055  pythagtriplem15  13087  pcpremul  13102  pcdiv  13111  pcqmul  13112  pcqdiv  13116  dvdsprmpweq  13144  sumhashdc  13156  pcfaclem  13158  qexpz  13161  ballotfilemfrcn0  13332  ctinf  13380  setsvala  13442  ressressg  13489  ressabsg  13490  rngbaseg  13550  ptex  13678  issubmnd  13815  ress0g  13816  imasmnd2  13819  grpasscan2  13929  grpidrcan  13930  grpidlcan  13931  grpinvadd  13943  grpsubeq0  13951  grppncan  13956  dfgrp3m  13964  grpsubpropd2  13970  imasgrp2  13973  mhmmnd  13979  mulgnegneg  14004  mulgaddcomlem  14008  mulgaddcom  14009  mulginvcom  14010  mulgmodid  14024  issubg  14036  nsgconj  14069  nsgid  14078  quselbasg  14093  quseccl0g  14094  ghmnsgima  14131  cmn4  14199  ablinvadd  14205  ablsub4  14208  abladdsub4  14209  ablpncan2  14211  gsumsncmn  14247  gsumconstcmn  14267  pwsinvg  14323  rngpropd  14362  imasrng  14363  issrg  14377  ringidss  14442  ringcom  14444  imasring  14479  unitmulcl  14530  unitmulclb  14531  dvrcl  14552  unitdvcl  14553  dvrcan1  14557  dvrcan3  14558  issubrng  14617  subrngpropd  14634  rrgeq0  14683  islmod  14737  lmodcom  14780  rmodislmodlem  14797  rmodislmod  14798  lss0cl  14816  lssvnegcl  14823  lssintclm  14831  lssincl  14832  lspss  14846  lspun  14849  lspsnvsi  14865  lsslsp  14876  rnglidlmmgm  14943  rnglidlmsgrp  14944  rnglidlrng  14945  qus2idrng  14972  qusmulrng  14979  assa2ass  15119  assa2ass2  15120  aspid  15127  aspss  15129  asclmul1  15139  asclmul2  15140  asclinvg  15142  psrbagdceq  15169  snifpsrbagfi  15170  psrbaglecl  15174  psrbagcon  15176  2basgeng  15320  clsss  15356  ntrss  15357  ntrin  15362  neiss  15388  restco  15412  restabs  15413  lmconst  15454  psmetsym  15567  psmetge0  15569  xmetge0  15603  xmetsym  15606  xmetresbl  15678  mopni3  15722  bdxmet  15739  bdmopn  15742  txmetcnp  15756  dvfvalap  15919  dvid  15933  dvidre  15935  dvcnp2cntop  15937  elplyr  15978  ply1term  15981  ptolemy  16063  logfac  16138  rpcxpadd  16150  rpmulcxp  16154  rpdivcxp  16156  cxpmul  16157  rpcxple2  16165  rpcxplt2  16166  cxpcom  16185  rplogbval  16193  rplogbcl  16194  rprelogbmulexp  16204  relogbexpap  16206  logbleb  16209  logblt  16210  rplogbcxp  16211  rpcxplogb  16212  sgmppw  16298  prmefexple  16320  lgslem1  16336  lgsfcl2  16342  lgsneg  16360  lgsne0  16374  lgssq2  16377  lgsdirnn0  16383  gausslemma2dlem1a  16394  lgsquad  16416  2lgsoddprmlem2  16442  funvtxvalg  16494  funiedgvalg  16495  lpvtx  16537  upgrex  16561  subumgredg2en  16729  iedginwlk  16815  eulerpathprum  16938  dichmul0or  16977