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  4464  elirr  4688  sotri2  5185  sotri3  5186  funtpg  5432  funimaexglem  5464  feq123  5525  ftpg  5899  fsnunf  5915  foco2  5959  fcofo  5990  f1oiso2  6033  riotass  6068  ovmpox  6217  ovmpoga  6218  caovimo  6283  ofeq  6305  ofrval  6313  fvn0elsuppb  6492  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  diffifi  7198  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  ssfidc  7245  iunfidisj  7260  fissfi  7263  sbthlemi9  7282  elfir  7307  fdcf1  7316  djuassen  7573  dftap2  7617  mulcanenq  7752  ltanqg  7767  addnnnq0  7816  distrlem4prl  7951  distrlem4pru  7952  distrprg  7955  aptipr  8008  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  mul31  8457  addsubass  8536  subcan2  8551  subsub2  8554  subsub4  8559  npncan3  8564  pnpcan  8565  pnncan  8567  subcan  8581  subdi  8712  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  lesubadd  8762  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  ltaddsublt  8900  gt0add  8902  apreap  8916  lemul1  8922  reapmul1lem  8923  reapmul1  8924  reapadd1  8925  remulext1  8928  remulext2  8929  apadd2  8938  mulext2  8942  mulap0r  8944  leltap  8954  ltap  8962  apsub1  8971  recexaplem2  8981  mulcanap  8994  mulcanap2  8995  divvalap  9005  divcanap2  9011  diveqap0  9013  divrecap  9019  divrecap2  9020  divdirap  9028  divcanap3  9029  div11ap  9031  muldivdirap  9038  divcanap5  9045  redivclap  9062  div2negap  9066  apmul1  9119  apmul2  9120  div2subap  9168  ltdiv1  9199  ltmuldiv  9205  lemuldiv  9212  lt2msq1  9216  ltdiv23  9223  lediv23  9224  squeeze0  9235  ofnegsub  9293  difgtsumgt  9716  zfidc  9725  gtndiv  9743  eluz2  9929  eluzsub  9954  peano2uz  9985  nn01to3  10019  divge1  10126  ledivge1le  10129  addlelt  10171  xaddass  10273  xleadd1  10279  xltadd1  10280  ixxssixx  10306  lbico1  10334  lbicc2  10388  icoshftf1o  10395  fzen  10449  fzrev3  10496  fzrevral2  10515  nelfzo  10561  elfzo0  10595  elfzo0z  10598  fzosplitprm1  10655  qbtwnre  10693  flqwordi  10725  flqword2  10726  adddivflid  10729  flltdivnn0lt  10741  modqcl  10765  mulqmod0  10769  modqmulnn  10781  modqabs2  10797  addmodid  10811  modifeq2int  10825  modqeqmodmin  10833  seqeq2  10890  seqeq3  10891  seq1g  10902  seqp1g  10905  exp3val  10980  expnegap0  10986  expgt1  11016  exprecap  11019  leexp2a  11031  expubnd  11035  sqdivap  11042  expnbnd  11103  mulsubdivbinom2ap  11151  bccmpl  11194  fihashss  11259  leisorel  11291  ccatass  11378  ccats1val2  11410  swrdval  11422  swrdval2  11425  swrdlen2  11436  swrdfv2  11437  pfxfv  11458  pfxn0  11462  pfxnd  11463  swrdswrd  11479  pfxswrd  11480  pfxpfx  11482  ccats1pfxeqbi  11516  s3cl  11560  s3fv0g  11565  s3fv1g  11566  s3fv2g  11567  shftfibg  11587  mulreap  11631  abssubne0  11859  maxleast  11981  lemininf  12002  ltmininf  12003  xrmaxltsup  12026  xrmaxaddlem  12028  xrmaxadd  12029  xrmineqinf  12037  xrltmininf  12038  xrminltinf  12040  xrminadd  12043  climuni  12061  reccn2ap  12081  isumz  12158  fsumsplitsnun  12188  geoisum1c  12289  prod1dc  12355  efltim  12467  dvdscmulr  12589  dvdsmulcr  12590  summodnegmod  12591  modmulconst  12592  dvdsmultr2  12602  dvdsexp  12630  mulmoddvds  12632  modremain  12698  divgcdz  12750  gcdaddm  12763  dvdsgcdb  12792  gcdass  12794  mulgcd  12795  gcddiv  12798  rplpwr  12806  uzwodc  12816  lcmdvdsb  12864  lcmass  12865  mulgcddvds  12874  qredeq  12876  qredeu  12877  rpmul  12878  divgcdcoprmex  12882  cncongr1  12883  rpexp  12933  rpexp12i  12935  odzcllem  13023  odzdvds  13026  odzphi  13027  pythagtriplem15  13059  pcpremul  13074  pcdiv  13083  pcqmul  13084  pcqdiv  13088  dvdsprmpweq  13116  sumhashdc  13128  pcfaclem  13130  qexpz  13133  ballotfilemfrcn0  13275  ctinf  13323  setsvala  13385  ressressg  13431  ressabsg  13432  rngbaseg  13492  ptex  13620  issubmnd  13757  ress0g  13758  imasmnd2  13761  grpasscan2  13871  grpidrcan  13872  grpidlcan  13873  grpinvadd  13885  grpsubeq0  13893  grppncan  13898  dfgrp3m  13906  grpsubpropd2  13912  imasgrp2  13915  mhmmnd  13921  mulgnegneg  13946  mulgaddcomlem  13950  mulgaddcom  13951  mulginvcom  13952  mulgmodid  13966  issubg  13978  nsgconj  14011  nsgid  14020  quselbasg  14035  quseccl0g  14036  ghmnsgima  14073  cmn4  14110  ablinvadd  14116  ablsub4  14119  abladdsub4  14120  ablpncan2  14122  gsumsncmn  14158  gsumconstcmn  14168  pwsinvg  14217  rngpropd  14256  imasrng  14257  issrg  14271  ringidss  14336  ringcom  14338  imasring  14371  unitmulcl  14422  unitmulclb  14423  dvrcl  14444  unitdvcl  14445  dvrcan1  14449  dvrcan3  14450  issubrng  14509  subrngpropd  14526  rrgeq0  14575  islmod  14629  lmodcom  14672  rmodislmodlem  14689  rmodislmod  14690  lss0cl  14708  lssvnegcl  14715  lssintclm  14723  lssincl  14724  lspss  14738  lspun  14741  lspsnvsi  14757  lsslsp  14768  rnglidlmmgm  14835  rnglidlmsgrp  14836  rnglidlrng  14837  qus2idrng  14864  qusmulrng  14871  assa2ass  15011  assa2ass2  15012  aspid  15019  aspss  15021  asclmul1  15031  asclmul2  15032  asclinvg  15034  psrbaglecl  15062  psrbagcon  15064  2basgeng  15185  clsss  15221  ntrss  15222  ntrin  15227  neiss  15253  restco  15277  restabs  15278  lmconst  15319  psmetsym  15432  psmetge0  15434  xmetge0  15468  xmetsym  15471  xmetresbl  15543  mopni3  15587  bdxmet  15604  bdmopn  15607  txmetcnp  15621  dvfvalap  15784  dvid  15798  dvidre  15800  dvcnp2cntop  15802  elplyr  15843  ply1term  15846  ptolemy  15928  logfac  16001  rpcxpadd  16013  rpmulcxp  16017  rpdivcxp  16019  cxpmul  16020  rpcxple2  16026  rpcxplt2  16027  cxpcom  16046  rplogbval  16053  rplogbcl  16054  rprelogbmulexp  16064  relogbexpap  16066  logbleb  16069  logblt  16070  rplogbcxp  16071  rpcxplogb  16072  sgmppw  16112  lgslem1  16131  lgsfcl2  16137  lgsneg  16155  lgsne0  16169  lgssq2  16172  lgsdirnn0  16178  gausslemma2dlem1a  16189  lgsquad  16211  2lgsoddprmlem2  16237  funvtxvalg  16289  funiedgvalg  16290  lpvtx  16332  upgrex  16356  subumgredg2en  16524  iedginwlk  16610  eulerpathprum  16733  dichmul0or  16772