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  4407  elirr  4630  sotri2  5122  sotri3  5123  funtpg  5368  funimaexglem  5400  feq123  5461  ftpg  5816  fsnunf  5832  foco2  5870  fcofo  5901  f1oiso2  5944  riotass  5977  ovmpox  6124  ovmpoga  6125  caovimo  6190  ofeq  6211  ofrval  6219  tfr1onlembxssdm  6479  tfrcllembxssdm  6492  frecsuclem  6542  frecrdg  6544  domssr  6919  mapxpen  6997  diffifi  7044  unsnfidcex  7070  unsnfidcel  7071  unfidisj  7072  undifdc  7074  ssfidc  7087  iunfidisj  7101  sbthlemi9  7120  elfir  7128  djuassen  7387  dftap2  7425  mulcanenq  7560  ltanqg  7575  addnnnq0  7624  distrlem4prl  7759  distrlem4pru  7760  distrprg  7763  aptipr  7816  addsrpr  7920  mulsrpr  7921  mulasssrg  7933  ltpsrprg  7978  axmulass  8048  axpre-ltadd  8061  mul31  8265  addsubass  8344  subcan2  8359  subsub2  8362  subsub4  8367  npncan3  8372  pnpcan  8373  pnncan  8375  subcan  8389  subdi  8519  ltadd1  8564  leadd1  8565  leadd2  8566  ltsubadd  8567  lesubadd  8569  ltaddsub  8571  leaddsub  8573  lesub1  8591  lesub2  8592  ltsub1  8593  ltsub2  8594  ltaddsublt  8706  gt0add  8708  apreap  8722  lemul1  8728  reapmul1lem  8729  reapmul1  8730  reapadd1  8731  remulext1  8734  remulext2  8735  apadd2  8744  mulext2  8748  mulap0r  8750  leltap  8760  ltap  8768  apsub1  8777  recexaplem2  8787  mulcanap  8800  mulcanap2  8801  divvalap  8809  divcanap2  8815  diveqap0  8817  divrecap  8823  divrecap2  8824  divdirap  8832  divcanap3  8833  div11ap  8835  muldivdirap  8842  divcanap5  8849  redivclap  8866  div2negap  8870  apmul1  8923  apmul2  8924  div2subap  8972  ltdiv1  9003  ltmuldiv  9009  lemuldiv  9016  lt2msq1  9020  ltdiv23  9027  lediv23  9028  squeeze0  9039  ofnegsub  9097  difgtsumgt  9504  gtndiv  9530  eluz2  9716  eluzsub  9740  peano2uz  9766  nn01to3  9800  divge1  9907  ledivge1le  9910  addlelt  9952  xaddass  10053  xleadd1  10059  xltadd1  10060  ixxssixx  10086  lbico1  10114  lbicc2  10168  icoshftf1o  10175  fzen  10227  fzrev3  10271  fzrevral2  10290  nelfzo  10336  elfzo0  10370  elfzo0z  10372  fzosplitprm1  10427  qbtwnre  10463  flqwordi  10495  flqword2  10496  adddivflid  10499  flltdivnn0lt  10511  modqcl  10535  mulqmod0  10539  modqmulnn  10551  modqabs2  10567  addmodid  10581  modifeq2int  10595  modqeqmodmin  10603  seqeq2  10660  seqeq3  10661  seq1g  10672  seqp1g  10675  exp3val  10750  expnegap0  10756  expgt1  10786  exprecap  10789  leexp2a  10801  expubnd  10805  sqdivap  10812  expnbnd  10872  mulsubdivbinom2ap  10920  bccmpl  10963  fihashss  11025  leisorel  11046  ccatass  11129  ccats1val2  11157  swrdval  11166  swrdval2  11169  swrdlen2  11180  swrdfv2  11181  pfxfv  11202  pfxn0  11206  pfxnd  11207  swrdswrd  11223  pfxswrd  11224  pfxpfx  11226  ccats1pfxeqbi  11260  s3cl  11304  s3fv0g  11309  s3fv1g  11310  shftfibg  11317  mulreap  11361  abssubne0  11588  maxleast  11710  lemininf  11731  ltmininf  11732  xrmaxltsup  11755  xrmaxaddlem  11757  xrmaxadd  11758  xrmineqinf  11766  xrltmininf  11767  xrminltinf  11769  xrminadd  11772  climuni  11790  reccn2ap  11810  isumz  11886  fsumsplitsnun  11916  geoisum1c  12017  prod1dc  12083  efltim  12195  dvdscmulr  12317  dvdsmulcr  12318  summodnegmod  12319  modmulconst  12320  dvdsmultr2  12330  dvdsexp  12358  mulmoddvds  12360  modremain  12426  divgcdz  12478  gcdaddm  12491  dvdsgcdb  12520  gcdass  12522  mulgcd  12523  gcddiv  12526  rplpwr  12534  uzwodc  12544  lcmdvdsb  12592  lcmass  12593  mulgcddvds  12602  qredeq  12604  qredeu  12605  rpmul  12606  divgcdcoprmex  12610  cncongr1  12611  rpexp  12661  rpexp12i  12663  odzcllem  12751  odzdvds  12754  odzphi  12755  pythagtriplem15  12787  pcpremul  12802  pcdiv  12811  pcqmul  12812  pcqdiv  12816  dvdsprmpweq  12844  sumhashdc  12856  pcfaclem  12858  qexpz  12861  ctinf  12987  setsvala  13049  ressressg  13094  ressabsg  13095  rngbaseg  13155  ptex  13283  issubmnd  13461  ress0g  13462  imasmnd2  13471  gsumfzz  13514  grpasscan2  13583  grpidrcan  13584  grpidlcan  13585  grpinvadd  13597  grpsubeq0  13605  grppncan  13610  dfgrp3m  13618  grpsubpropd2  13624  pwsinvg  13631  imasgrp2  13633  mhmmnd  13639  mulgnegneg  13664  mulgaddcomlem  13668  mulgaddcom  13669  mulginvcom  13670  mulgmodid  13684  issubg  13696  nsgconj  13729  nsgid  13738  quselbasg  13753  quseccl0g  13754  ghmnsgima  13791  cmn4  13828  ablinvadd  13833  ablsub4  13836  abladdsub4  13837  ablpncan2  13839  rngpropd  13904  imasrng  13905  issrg  13914  ringidss  13978  ringcom  13980  imasring  14013  unitmulcl  14062  unitmulclb  14063  dvrcl  14084  unitdvcl  14085  dvrcan1  14089  dvrcan3  14090  issubrng  14148  subrngpropd  14165  rrgeq0  14214  islmod  14240  lmodcom  14282  rmodislmodlem  14299  rmodislmod  14300  lss0cl  14318  lssvnegcl  14325  lssintclm  14333  lssincl  14334  lspss  14348  lspun  14351  lspsnvsi  14367  lsslsp  14378  rnglidlmmgm  14445  rnglidlmsgrp  14446  rnglidlrng  14447  qus2idrng  14474  qusmulrng  14481  2basgeng  14741  clsss  14777  ntrss  14778  ntrin  14783  neiss  14809  restco  14833  restabs  14834  lmconst  14875  psmetsym  14988  psmetge0  14990  xmetge0  15024  xmetsym  15027  xmetresbl  15099  mopni3  15143  bdxmet  15160  bdmopn  15163  txmetcnp  15177  dvfvalap  15340  dvid  15354  dvidre  15356  dvcnp2cntop  15358  elplyr  15399  ply1term  15402  ptolemy  15483  rpcxpadd  15564  rpmulcxp  15568  rpdivcxp  15570  cxpmul  15571  rpcxple2  15577  rpcxplt2  15578  cxpcom  15597  rplogbval  15604  rplogbcl  15605  rprelogbmulexp  15615  relogbexpap  15617  logbleb  15620  logblt  15621  rplogbcxp  15622  rpcxplogb  15623  sgmppw  15651  lgslem1  15664  lgsfcl2  15670  lgsneg  15688  lgsne0  15702  lgssq2  15705  lgsdirnn0  15711  gausslemma2dlem1a  15722  lgsquad  15744  2lgsoddprmlem2  15770  funvtxvalg  15822  funiedgvalg  15823  lpvtx  15864  upgrex  15888