Theorem simp1 1021

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 1018	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simpld 112	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)

Syntax hints:   → wi 4   ∧ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  simpl1  1024  simpr1  1027  simp1i  1030  simp1d  1033  simp11  1051  simp21  1054  simp31  1057  syld3an3  1316  3ianorr  1343  intn3an1d  1390  stoic4a  1474  stoic4b  1475  rsp2e  2581  ifnetruedc  3647  issod  4414  elirr  4637  sotri2  5132  sotri3  5133  funtpg  5378  funimaexglem  5410  feq123  5471  ftpg  5833  fsnunf  5849  foco2  5889  fcofo  5920  f1oiso2  5963  riotass  5996  ovmpox  6145  ovmpoga  6146  caovimo  6211  ofeq  6233  ofrval  6241  tfr1onlembxssdm  6504  tfrcllembxssdm  6517  frecsuclem  6567  frecrdg  6569  domssr  6946  mapxpen  7029  diffifi  7078  unsnfidcex  7107  unsnfidcel  7108  unfidisj  7109  undifdc  7111  ssfidc  7124  iunfidisj  7139  sbthlemi9  7158  elfir  7166  djuassen  7425  dftap2  7463  mulcanenq  7598  ltanqg  7613  addnnnq0  7662  distrlem4prl  7797  distrlem4pru  7798  distrprg  7801  aptipr  7854  addsrpr  7958  mulsrpr  7959  mulasssrg  7971  ltpsrprg  8016  axmulass  8086  axpre-ltadd  8099  mul31  8303  addsubass  8382  subcan2  8397  subsub2  8400  subsub4  8405  npncan3  8410  pnpcan  8411  pnncan  8413  subcan  8427  subdi  8557  ltadd1  8602  leadd1  8603  leadd2  8604  ltsubadd  8605  lesubadd  8607  ltaddsub  8609  leaddsub  8611  lesub1  8629  lesub2  8630  ltsub1  8631  ltsub2  8632  ltaddsublt  8744  gt0add  8746  apreap  8760  lemul1  8766  reapmul1lem  8767  reapmul1  8768  reapadd1  8769  remulext1  8772  remulext2  8773  apadd2  8782  mulext2  8786  mulap0r  8788  leltap  8798  ltap  8806  apsub1  8815  recexaplem2  8825  mulcanap  8838  mulcanap2  8839  divvalap  8847  divcanap2  8853  diveqap0  8855  divrecap  8861  divrecap2  8862  divdirap  8870  divcanap3  8871  div11ap  8873  muldivdirap  8880  divcanap5  8887  redivclap  8904  div2negap  8908  apmul1  8961  apmul2  8962  div2subap  9010  ltdiv1  9041  ltmuldiv  9047  lemuldiv  9054  lt2msq1  9058  ltdiv23  9065  lediv23  9066  squeeze0  9077  ofnegsub  9135  difgtsumgt  9542  gtndiv  9568  eluz2  9754  eluzsub  9779  peano2uz  9810  nn01to3  9844  divge1  9951  ledivge1le  9954  addlelt  9996  xaddass  10097  xleadd1  10103  xltadd1  10104  ixxssixx  10130  lbico1  10158  lbicc2  10212  icoshftf1o  10219  fzen  10271  fzrev3  10315  fzrevral2  10334  nelfzo  10380  elfzo0  10414  elfzo0z  10416  fzosplitprm1  10473  qbtwnre  10509  flqwordi  10541  flqword2  10542  adddivflid  10545  flltdivnn0lt  10557  modqcl  10581  mulqmod0  10585  modqmulnn  10597  modqabs2  10613  addmodid  10627  modifeq2int  10641  modqeqmodmin  10649  seqeq2  10706  seqeq3  10707  seq1g  10718  seqp1g  10721  exp3val  10796  expnegap0  10802  expgt1  10832  exprecap  10835  leexp2a  10847  expubnd  10851  sqdivap  10858  expnbnd  10918  mulsubdivbinom2ap  10966  bccmpl  11009  fihashss  11073  leisorel  11094  ccatass  11178  ccats1val2  11210  swrdval  11222  swrdval2  11225  swrdlen2  11236  swrdfv2  11237  pfxfv  11258  pfxn0  11262  pfxnd  11263  swrdswrd  11279  pfxswrd  11280  pfxpfx  11282  ccats1pfxeqbi  11316  s3cl  11360  s3fv0g  11365  s3fv1g  11366  s3fv2g  11367  shftfibg  11374  mulreap  11418  abssubne0  11645  maxleast  11767  lemininf  11788  ltmininf  11789  xrmaxltsup  11812  xrmaxaddlem  11814  xrmaxadd  11815  xrmineqinf  11823  xrltmininf  11824  xrminltinf  11826  xrminadd  11829  climuni  11847  reccn2ap  11867  isumz  11943  fsumsplitsnun  11973  geoisum1c  12074  prod1dc  12140  efltim  12252  dvdscmulr  12374  dvdsmulcr  12375  summodnegmod  12376  modmulconst  12377  dvdsmultr2  12387  dvdsexp  12415  mulmoddvds  12417  modremain  12483  divgcdz  12535  gcdaddm  12548  dvdsgcdb  12577  gcdass  12579  mulgcd  12580  gcddiv  12583  rplpwr  12591  uzwodc  12601  lcmdvdsb  12649  lcmass  12650  mulgcddvds  12659  qredeq  12661  qredeu  12662  rpmul  12663  divgcdcoprmex  12667  cncongr1  12668  rpexp  12718  rpexp12i  12720  odzcllem  12808  odzdvds  12811  odzphi  12812  pythagtriplem15  12844  pcpremul  12859  pcdiv  12868  pcqmul  12869  pcqdiv  12873  dvdsprmpweq  12901  sumhashdc  12913  pcfaclem  12915  qexpz  12918  ctinf  13044  setsvala  13106  ressressg  13151  ressabsg  13152  rngbaseg  13212  ptex  13340  issubmnd  13518  ress0g  13519  imasmnd2  13528  gsumfzz  13571  grpasscan2  13640  grpidrcan  13641  grpidlcan  13642  grpinvadd  13654  grpsubeq0  13662  grppncan  13667  dfgrp3m  13675  grpsubpropd2  13681  pwsinvg  13688  imasgrp2  13690  mhmmnd  13696  mulgnegneg  13721  mulgaddcomlem  13725  mulgaddcom  13726  mulginvcom  13727  mulgmodid  13741  issubg  13753  nsgconj  13786  nsgid  13795  quselbasg  13810  quseccl0g  13811  ghmnsgima  13848  cmn4  13885  ablinvadd  13890  ablsub4  13893  abladdsub4  13894  ablpncan2  13896  rngpropd  13961  imasrng  13962  issrg  13971  ringidss  14035  ringcom  14037  imasring  14070  unitmulcl  14120  unitmulclb  14121  dvrcl  14142  unitdvcl  14143  dvrcan1  14147  dvrcan3  14148  issubrng  14206  subrngpropd  14223  rrgeq0  14272  islmod  14298  lmodcom  14340  rmodislmodlem  14357  rmodislmod  14358  lss0cl  14376  lssvnegcl  14383  lssintclm  14391  lssincl  14392  lspss  14406  lspun  14409  lspsnvsi  14425  lsslsp  14436  rnglidlmmgm  14503  rnglidlmsgrp  14504  rnglidlrng  14505  qus2idrng  14532  qusmulrng  14539  2basgeng  14799  clsss  14835  ntrss  14836  ntrin  14841  neiss  14867  restco  14891  restabs  14892  lmconst  14933  psmetsym  15046  psmetge0  15048  xmetge0  15082  xmetsym  15085  xmetresbl  15157  mopni3  15201  bdxmet  15218  bdmopn  15221  txmetcnp  15235  dvfvalap  15398  dvid  15412  dvidre  15414  dvcnp2cntop  15416  elplyr  15457  ply1term  15460  ptolemy  15541  rpcxpadd  15622  rpmulcxp  15626  rpdivcxp  15628  cxpmul  15629  rpcxple2  15635  rpcxplt2  15636  cxpcom  15655  rplogbval  15662  rplogbcl  15663  rprelogbmulexp  15673  relogbexpap  15675  logbleb  15678  logblt  15679  rplogbcxp  15680  rpcxplogb  15681  sgmppw  15709  lgslem1  15722  lgsfcl2  15728  lgsneg  15746  lgsne0  15760  lgssq2  15763  lgsdirnn0  15769  gausslemma2dlem1a  15780  lgsquad  15802  2lgsoddprmlem2  15828  funvtxvalg  15880  funiedgvalg  15881  lpvtx  15923  upgrex  15947  iedginwlk  16168