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  3646  issod  4410  elirr  4633  sotri2  5126  sotri3  5127  funtpg  5372  funimaexglem  5404  feq123  5465  ftpg  5827  fsnunf  5843  foco2  5883  fcofo  5914  f1oiso2  5957  riotass  5990  ovmpox  6139  ovmpoga  6140  caovimo  6205  ofeq  6227  ofrval  6235  tfr1onlembxssdm  6495  tfrcllembxssdm  6508  frecsuclem  6558  frecrdg  6560  domssr  6937  mapxpen  7017  diffifi  7064  unsnfidcex  7090  unsnfidcel  7091  unfidisj  7092  undifdc  7094  ssfidc  7107  iunfidisj  7121  sbthlemi9  7140  elfir  7148  djuassen  7407  dftap2  7445  mulcanenq  7580  ltanqg  7595  addnnnq0  7644  distrlem4prl  7779  distrlem4pru  7780  distrprg  7783  aptipr  7836  addsrpr  7940  mulsrpr  7941  mulasssrg  7953  ltpsrprg  7998  axmulass  8068  axpre-ltadd  8081  mul31  8285  addsubass  8364  subcan2  8379  subsub2  8382  subsub4  8387  npncan3  8392  pnpcan  8393  pnncan  8395  subcan  8409  subdi  8539  ltadd1  8584  leadd1  8585  leadd2  8586  ltsubadd  8587  lesubadd  8589  ltaddsub  8591  leaddsub  8593  lesub1  8611  lesub2  8612  ltsub1  8613  ltsub2  8614  ltaddsublt  8726  gt0add  8728  apreap  8742  lemul1  8748  reapmul1lem  8749  reapmul1  8750  reapadd1  8751  remulext1  8754  remulext2  8755  apadd2  8764  mulext2  8768  mulap0r  8770  leltap  8780  ltap  8788  apsub1  8797  recexaplem2  8807  mulcanap  8820  mulcanap2  8821  divvalap  8829  divcanap2  8835  diveqap0  8837  divrecap  8843  divrecap2  8844  divdirap  8852  divcanap3  8853  div11ap  8855  muldivdirap  8862  divcanap5  8869  redivclap  8886  div2negap  8890  apmul1  8943  apmul2  8944  div2subap  8992  ltdiv1  9023  ltmuldiv  9029  lemuldiv  9036  lt2msq1  9040  ltdiv23  9047  lediv23  9048  squeeze0  9059  ofnegsub  9117  difgtsumgt  9524  gtndiv  9550  eluz2  9736  eluzsub  9760  peano2uz  9786  nn01to3  9820  divge1  9927  ledivge1le  9930  addlelt  9972  xaddass  10073  xleadd1  10079  xltadd1  10080  ixxssixx  10106  lbico1  10134  lbicc2  10188  icoshftf1o  10195  fzen  10247  fzrev3  10291  fzrevral2  10310  nelfzo  10356  elfzo0  10390  elfzo0z  10392  fzosplitprm1  10448  qbtwnre  10484  flqwordi  10516  flqword2  10517  adddivflid  10520  flltdivnn0lt  10532  modqcl  10556  mulqmod0  10560  modqmulnn  10572  modqabs2  10588  addmodid  10602  modifeq2int  10616  modqeqmodmin  10624  seqeq2  10681  seqeq3  10682  seq1g  10693  seqp1g  10696  exp3val  10771  expnegap0  10777  expgt1  10807  exprecap  10810  leexp2a  10822  expubnd  10826  sqdivap  10833  expnbnd  10893  mulsubdivbinom2ap  10941  bccmpl  10984  fihashss  11046  leisorel  11067  ccatass  11151  ccats1val2  11179  swrdval  11188  swrdval2  11191  swrdlen2  11202  swrdfv2  11203  pfxfv  11224  pfxn0  11228  pfxnd  11229  swrdswrd  11245  pfxswrd  11246  pfxpfx  11248  ccats1pfxeqbi  11282  s3cl  11326  s3fv0g  11331  s3fv1g  11332  shftfibg  11339  mulreap  11383  abssubne0  11610  maxleast  11732  lemininf  11753  ltmininf  11754  xrmaxltsup  11777  xrmaxaddlem  11779  xrmaxadd  11780  xrmineqinf  11788  xrltmininf  11789  xrminltinf  11791  xrminadd  11794  climuni  11812  reccn2ap  11832  isumz  11908  fsumsplitsnun  11938  geoisum1c  12039  prod1dc  12105  efltim  12217  dvdscmulr  12339  dvdsmulcr  12340  summodnegmod  12341  modmulconst  12342  dvdsmultr2  12352  dvdsexp  12380  mulmoddvds  12382  modremain  12448  divgcdz  12500  gcdaddm  12513  dvdsgcdb  12542  gcdass  12544  mulgcd  12545  gcddiv  12548  rplpwr  12556  uzwodc  12566  lcmdvdsb  12614  lcmass  12615  mulgcddvds  12624  qredeq  12626  qredeu  12627  rpmul  12628  divgcdcoprmex  12632  cncongr1  12633  rpexp  12683  rpexp12i  12685  odzcllem  12773  odzdvds  12776  odzphi  12777  pythagtriplem15  12809  pcpremul  12824  pcdiv  12833  pcqmul  12834  pcqdiv  12838  dvdsprmpweq  12866  sumhashdc  12878  pcfaclem  12880  qexpz  12883  ctinf  13009  setsvala  13071  ressressg  13116  ressabsg  13117  rngbaseg  13177  ptex  13305  issubmnd  13483  ress0g  13484  imasmnd2  13493  gsumfzz  13536  grpasscan2  13605  grpidrcan  13606  grpidlcan  13607  grpinvadd  13619  grpsubeq0  13627  grppncan  13632  dfgrp3m  13640  grpsubpropd2  13646  pwsinvg  13653  imasgrp2  13655  mhmmnd  13661  mulgnegneg  13686  mulgaddcomlem  13690  mulgaddcom  13691  mulginvcom  13692  mulgmodid  13706  issubg  13718  nsgconj  13751  nsgid  13760  quselbasg  13775  quseccl0g  13776  ghmnsgima  13813  cmn4  13850  ablinvadd  13855  ablsub4  13858  abladdsub4  13859  ablpncan2  13861  rngpropd  13926  imasrng  13927  issrg  13936  ringidss  14000  ringcom  14002  imasring  14035  unitmulcl  14085  unitmulclb  14086  dvrcl  14107  unitdvcl  14108  dvrcan1  14112  dvrcan3  14113  issubrng  14171  subrngpropd  14188  rrgeq0  14237  islmod  14263  lmodcom  14305  rmodislmodlem  14322  rmodislmod  14323  lss0cl  14341  lssvnegcl  14348  lssintclm  14356  lssincl  14357  lspss  14371  lspun  14374  lspsnvsi  14390  lsslsp  14401  rnglidlmmgm  14468  rnglidlmsgrp  14469  rnglidlrng  14470  qus2idrng  14497  qusmulrng  14504  2basgeng  14764  clsss  14800  ntrss  14801  ntrin  14806  neiss  14832  restco  14856  restabs  14857  lmconst  14898  psmetsym  15011  psmetge0  15013  xmetge0  15047  xmetsym  15050  xmetresbl  15122  mopni3  15166  bdxmet  15183  bdmopn  15186  txmetcnp  15200  dvfvalap  15363  dvid  15377  dvidre  15379  dvcnp2cntop  15381  elplyr  15422  ply1term  15425  ptolemy  15506  rpcxpadd  15587  rpmulcxp  15591  rpdivcxp  15593  cxpmul  15594  rpcxple2  15600  rpcxplt2  15601  cxpcom  15620  rplogbval  15627  rplogbcl  15628  rprelogbmulexp  15638  relogbexpap  15640  logbleb  15643  logblt  15644  rplogbcxp  15645  rpcxplogb  15646  sgmppw  15674  lgslem1  15687  lgsfcl2  15693  lgsneg  15711  lgsne0  15725  lgssq2  15728  lgsdirnn0  15734  gausslemma2dlem1a  15745  lgsquad  15767  2lgsoddprmlem2  15793  funvtxvalg  15845  funiedgvalg  15846  lpvtx  15887  upgrex  15911  iedginwlk  16078