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  4411  elirr  4634  sotri2  5129  sotri3  5130  funtpg  5375  funimaexglem  5407  feq123  5468  ftpg  5830  fsnunf  5846  foco2  5886  fcofo  5917  f1oiso2  5960  riotass  5993  ovmpox  6142  ovmpoga  6143  caovimo  6208  ofeq  6230  ofrval  6238  tfr1onlembxssdm  6500  tfrcllembxssdm  6513  frecsuclem  6563  frecrdg  6565  domssr  6942  mapxpen  7022  diffifi  7069  unsnfidcex  7098  unsnfidcel  7099  unfidisj  7100  undifdc  7102  ssfidc  7115  iunfidisj  7129  sbthlemi9  7148  elfir  7156  djuassen  7415  dftap2  7453  mulcanenq  7588  ltanqg  7603  addnnnq0  7652  distrlem4prl  7787  distrlem4pru  7788  distrprg  7791  aptipr  7844  addsrpr  7948  mulsrpr  7949  mulasssrg  7961  ltpsrprg  8006  axmulass  8076  axpre-ltadd  8089  mul31  8293  addsubass  8372  subcan2  8387  subsub2  8390  subsub4  8395  npncan3  8400  pnpcan  8401  pnncan  8403  subcan  8417  subdi  8547  ltadd1  8592  leadd1  8593  leadd2  8594  ltsubadd  8595  lesubadd  8597  ltaddsub  8599  leaddsub  8601  lesub1  8619  lesub2  8620  ltsub1  8621  ltsub2  8622  ltaddsublt  8734  gt0add  8736  apreap  8750  lemul1  8756  reapmul1lem  8757  reapmul1  8758  reapadd1  8759  remulext1  8762  remulext2  8763  apadd2  8772  mulext2  8776  mulap0r  8778  leltap  8788  ltap  8796  apsub1  8805  recexaplem2  8815  mulcanap  8828  mulcanap2  8829  divvalap  8837  divcanap2  8843  diveqap0  8845  divrecap  8851  divrecap2  8852  divdirap  8860  divcanap3  8861  div11ap  8863  muldivdirap  8870  divcanap5  8877  redivclap  8894  div2negap  8898  apmul1  8951  apmul2  8952  div2subap  9000  ltdiv1  9031  ltmuldiv  9037  lemuldiv  9044  lt2msq1  9048  ltdiv23  9055  lediv23  9056  squeeze0  9067  ofnegsub  9125  difgtsumgt  9532  gtndiv  9558  eluz2  9744  eluzsub  9769  peano2uz  9795  nn01to3  9829  divge1  9936  ledivge1le  9939  addlelt  9981  xaddass  10082  xleadd1  10088  xltadd1  10089  ixxssixx  10115  lbico1  10143  lbicc2  10197  icoshftf1o  10204  fzen  10256  fzrev3  10300  fzrevral2  10319  nelfzo  10365  elfzo0  10399  elfzo0z  10401  fzosplitprm1  10457  qbtwnre  10493  flqwordi  10525  flqword2  10526  adddivflid  10529  flltdivnn0lt  10541  modqcl  10565  mulqmod0  10569  modqmulnn  10581  modqabs2  10597  addmodid  10611  modifeq2int  10625  modqeqmodmin  10633  seqeq2  10690  seqeq3  10691  seq1g  10702  seqp1g  10705  exp3val  10780  expnegap0  10786  expgt1  10816  exprecap  10819  leexp2a  10831  expubnd  10835  sqdivap  10842  expnbnd  10902  mulsubdivbinom2ap  10950  bccmpl  10993  fihashss  11056  leisorel  11077  ccatass  11161  ccats1val2  11192  swrdval  11201  swrdval2  11204  swrdlen2  11215  swrdfv2  11216  pfxfv  11237  pfxn0  11241  pfxnd  11242  swrdswrd  11258  pfxswrd  11259  pfxpfx  11261  ccats1pfxeqbi  11295  s3cl  11339  s3fv0g  11344  s3fv1g  11345  shftfibg  11352  mulreap  11396  abssubne0  11623  maxleast  11745  lemininf  11766  ltmininf  11767  xrmaxltsup  11790  xrmaxaddlem  11792  xrmaxadd  11793  xrmineqinf  11801  xrltmininf  11802  xrminltinf  11804  xrminadd  11807  climuni  11825  reccn2ap  11845  isumz  11921  fsumsplitsnun  11951  geoisum1c  12052  prod1dc  12118  efltim  12230  dvdscmulr  12352  dvdsmulcr  12353  summodnegmod  12354  modmulconst  12355  dvdsmultr2  12365  dvdsexp  12393  mulmoddvds  12395  modremain  12461  divgcdz  12513  gcdaddm  12526  dvdsgcdb  12555  gcdass  12557  mulgcd  12558  gcddiv  12561  rplpwr  12569  uzwodc  12579  lcmdvdsb  12627  lcmass  12628  mulgcddvds  12637  qredeq  12639  qredeu  12640  rpmul  12641  divgcdcoprmex  12645  cncongr1  12646  rpexp  12696  rpexp12i  12698  odzcllem  12786  odzdvds  12789  odzphi  12790  pythagtriplem15  12822  pcpremul  12837  pcdiv  12846  pcqmul  12847  pcqdiv  12851  dvdsprmpweq  12879  sumhashdc  12891  pcfaclem  12893  qexpz  12896  ctinf  13022  setsvala  13084  ressressg  13129  ressabsg  13130  rngbaseg  13190  ptex  13318  issubmnd  13496  ress0g  13497  imasmnd2  13506  gsumfzz  13549  grpasscan2  13618  grpidrcan  13619  grpidlcan  13620  grpinvadd  13632  grpsubeq0  13640  grppncan  13645  dfgrp3m  13653  grpsubpropd2  13659  pwsinvg  13666  imasgrp2  13668  mhmmnd  13674  mulgnegneg  13699  mulgaddcomlem  13703  mulgaddcom  13704  mulginvcom  13705  mulgmodid  13719  issubg  13731  nsgconj  13764  nsgid  13773  quselbasg  13788  quseccl0g  13789  ghmnsgima  13826  cmn4  13863  ablinvadd  13868  ablsub4  13871  abladdsub4  13872  ablpncan2  13874  rngpropd  13939  imasrng  13940  issrg  13949  ringidss  14013  ringcom  14015  imasring  14048  unitmulcl  14098  unitmulclb  14099  dvrcl  14120  unitdvcl  14121  dvrcan1  14125  dvrcan3  14126  issubrng  14184  subrngpropd  14201  rrgeq0  14250  islmod  14276  lmodcom  14318  rmodislmodlem  14335  rmodislmod  14336  lss0cl  14354  lssvnegcl  14361  lssintclm  14369  lssincl  14370  lspss  14384  lspun  14387  lspsnvsi  14403  lsslsp  14414  rnglidlmmgm  14481  rnglidlmsgrp  14482  rnglidlrng  14483  qus2idrng  14510  qusmulrng  14517  2basgeng  14777  clsss  14813  ntrss  14814  ntrin  14819  neiss  14845  restco  14869  restabs  14870  lmconst  14911  psmetsym  15024  psmetge0  15026  xmetge0  15060  xmetsym  15063  xmetresbl  15135  mopni3  15179  bdxmet  15196  bdmopn  15199  txmetcnp  15213  dvfvalap  15376  dvid  15390  dvidre  15392  dvcnp2cntop  15394  elplyr  15435  ply1term  15438  ptolemy  15519  rpcxpadd  15600  rpmulcxp  15604  rpdivcxp  15606  cxpmul  15607  rpcxple2  15613  rpcxplt2  15614  cxpcom  15633  rplogbval  15640  rplogbcl  15641  rprelogbmulexp  15651  relogbexpap  15653  logbleb  15656  logblt  15657  rplogbcxp  15658  rpcxplogb  15659  sgmppw  15687  lgslem1  15700  lgsfcl2  15706  lgsneg  15724  lgsne0  15738  lgssq2  15741  lgsdirnn0  15747  gausslemma2dlem1a  15758  lgsquad  15780  2lgsoddprmlem2  15806  funvtxvalg  15858  funiedgvalg  15859  lpvtx  15900  upgrex  15924  iedginwlk  16129