Theorem simp1 1024

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl1  1027  simpr1  1030  simp1i  1033  simp1d  1036  simp11  1054  simp21  1057  simp31  1060  syld3an3  1319  3ianorr  1346  intn3an1d  1393  stoic4a  1477  stoic4b  1478  rsp2e  2593  ifnetruedc  3665  issod  4439  elirr  4662  sotri2  5159  sotri3  5160  funtpg  5406  funimaexglem  5438  feq123  5499  ftpg  5867  fsnunf  5883  foco2  5925  fcofo  5956  f1oiso2  5999  riotass  6032  ovmpox  6181  ovmpoga  6182  caovimo  6247  ofeq  6268  ofrval  6276  fvn0elsuppb  6451  tfr1onlembxssdm  6573  tfrcllembxssdm  6586  frecsuclem  6636  frecrdg  6638  domssr  7016  mapxpen  7100  diffifi  7150  unsnfidcex  7179  unsnfidcel  7180  unfidisj  7181  undifdc  7183  ssfidc  7197  iunfidisj  7212  fissfi  7215  sbthlemi9  7234  elfir  7259  djuassen  7523  dftap2  7564  mulcanenq  7699  ltanqg  7714  addnnnq0  7763  distrlem4prl  7898  distrlem4pru  7899  distrprg  7902  aptipr  7955  addsrpr  8059  mulsrpr  8060  mulasssrg  8072  ltpsrprg  8117  axmulass  8187  axpre-ltadd  8200  mul31  8403  addsubass  8482  subcan2  8497  subsub2  8500  subsub4  8505  npncan3  8510  pnpcan  8511  pnncan  8513  subcan  8527  subdi  8657  ltadd1  8702  leadd1  8703  leadd2  8704  ltsubadd  8705  lesubadd  8707  ltaddsub  8709  leaddsub  8711  lesub1  8729  lesub2  8730  ltsub1  8731  ltsub2  8732  ltaddsublt  8844  gt0add  8846  apreap  8860  lemul1  8866  reapmul1lem  8867  reapmul1  8868  reapadd1  8869  remulext1  8872  remulext2  8873  apadd2  8882  mulext2  8886  mulap0r  8888  leltap  8898  ltap  8906  apsub1  8915  recexaplem2  8925  mulcanap  8938  mulcanap2  8939  divvalap  8947  divcanap2  8953  diveqap0  8955  divrecap  8961  divrecap2  8962  divdirap  8970  divcanap3  8971  div11ap  8973  muldivdirap  8980  divcanap5  8987  redivclap  9004  div2negap  9008  apmul1  9061  apmul2  9062  div2subap  9110  ltdiv1  9141  ltmuldiv  9147  lemuldiv  9154  lt2msq1  9158  ltdiv23  9165  lediv23  9166  squeeze0  9177  ofnegsub  9235  difgtsumgt  9646  gtndiv  9672  eluz2  9858  eluzsub  9883  peano2uz  9914  nn01to3  9948  divge1  10055  ledivge1le  10058  addlelt  10100  xaddass  10201  xleadd1  10207  xltadd1  10208  ixxssixx  10234  lbico1  10262  lbicc2  10316  icoshftf1o  10323  fzen  10376  fzrev3  10420  fzrevral2  10439  nelfzo  10485  elfzo0  10519  elfzo0z  10522  fzosplitprm1  10579  qbtwnre  10615  flqwordi  10647  flqword2  10648  adddivflid  10651  flltdivnn0lt  10663  modqcl  10687  mulqmod0  10691  modqmulnn  10703  modqabs2  10719  addmodid  10733  modifeq2int  10747  modqeqmodmin  10755  seqeq2  10812  seqeq3  10813  seq1g  10824  seqp1g  10827  exp3val  10902  expnegap0  10908  expgt1  10938  exprecap  10941  leexp2a  10953  expubnd  10957  sqdivap  10964  expnbnd  11024  mulsubdivbinom2ap  11072  bccmpl  11115  fihashss  11179  leisorel  11205  ccatass  11292  ccats1val2  11324  swrdval  11336  swrdval2  11339  swrdlen2  11350  swrdfv2  11351  pfxfv  11372  pfxn0  11376  pfxnd  11377  swrdswrd  11393  pfxswrd  11394  pfxpfx  11396  ccats1pfxeqbi  11430  s3cl  11474  s3fv0g  11479  s3fv1g  11480  s3fv2g  11481  shftfibg  11501  mulreap  11545  abssubne0  11772  maxleast  11894  lemininf  11915  ltmininf  11916  xrmaxltsup  11939  xrmaxaddlem  11941  xrmaxadd  11942  xrmineqinf  11950  xrltmininf  11951  xrminltinf  11953  xrminadd  11956  climuni  11974  reccn2ap  11994  isumz  12071  fsumsplitsnun  12101  geoisum1c  12202  prod1dc  12268  efltim  12380  dvdscmulr  12502  dvdsmulcr  12503  summodnegmod  12504  modmulconst  12505  dvdsmultr2  12515  dvdsexp  12543  mulmoddvds  12545  modremain  12611  divgcdz  12663  gcdaddm  12676  dvdsgcdb  12705  gcdass  12707  mulgcd  12708  gcddiv  12711  rplpwr  12719  uzwodc  12729  lcmdvdsb  12777  lcmass  12778  mulgcddvds  12787  qredeq  12789  qredeu  12790  rpmul  12791  divgcdcoprmex  12795  cncongr1  12796  rpexp  12846  rpexp12i  12848  odzcllem  12936  odzdvds  12939  odzphi  12940  pythagtriplem15  12972  pcpremul  12987  pcdiv  12996  pcqmul  12997  pcqdiv  13001  dvdsprmpweq  13029  sumhashdc  13041  pcfaclem  13043  qexpz  13046  ctinf  13173  setsvala  13235  ressressg  13280  ressabsg  13281  rngbaseg  13341  ptex  13469  issubmnd  13647  ress0g  13648  imasmnd2  13657  gsumfzz  13700  grpasscan2  13769  grpidrcan  13770  grpidlcan  13771  grpinvadd  13783  grpsubeq0  13791  grppncan  13796  dfgrp3m  13804  grpsubpropd2  13810  pwsinvg  13817  imasgrp2  13819  mhmmnd  13825  mulgnegneg  13850  mulgaddcomlem  13854  mulgaddcom  13855  mulginvcom  13856  mulgmodid  13870  issubg  13882  nsgconj  13915  nsgid  13924  quselbasg  13939  quseccl0g  13940  ghmnsgima  13977  cmn4  14014  ablinvadd  14019  ablsub4  14022  abladdsub4  14023  ablpncan2  14025  rngpropd  14091  imasrng  14092  issrg  14101  ringidss  14165  ringcom  14167  imasring  14200  unitmulcl  14250  unitmulclb  14251  dvrcl  14272  unitdvcl  14273  dvrcan1  14277  dvrcan3  14278  issubrng  14336  subrngpropd  14353  rrgeq0  14402  islmod  14431  lmodcom  14473  rmodislmodlem  14490  rmodislmod  14491  lss0cl  14509  lssvnegcl  14516  lssintclm  14524  lssincl  14525  lspss  14539  lspun  14542  lspsnvsi  14558  lsslsp  14569  rnglidlmmgm  14636  rnglidlmsgrp  14637  rnglidlrng  14638  qus2idrng  14665  qusmulrng  14672  psrbaglecl  14816  psrbagcon  14818  2basgeng  14939  clsss  14975  ntrss  14976  ntrin  14981  neiss  15007  restco  15031  restabs  15032  lmconst  15073  psmetsym  15186  psmetge0  15188  xmetge0  15222  xmetsym  15225  xmetresbl  15297  mopni3  15341  bdxmet  15358  bdmopn  15361  txmetcnp  15375  dvfvalap  15538  dvid  15552  dvidre  15554  dvcnp2cntop  15556  elplyr  15597  ply1term  15600  ptolemy  15681  rpcxpadd  15762  rpmulcxp  15766  rpdivcxp  15768  cxpmul  15769  rpcxple2  15775  rpcxplt2  15776  cxpcom  15795  rplogbval  15802  rplogbcl  15803  rprelogbmulexp  15813  relogbexpap  15815  logbleb  15818  logblt  15819  rplogbcxp  15820  rpcxplogb  15821  sgmppw  15852  lgslem1  15865  lgsfcl2  15871  lgsneg  15889  lgsne0  15903  lgssq2  15906  lgsdirnn0  15912  gausslemma2dlem1a  15923  lgsquad  15945  2lgsoddprmlem2  15971  funvtxvalg  16023  funiedgvalg  16024  lpvtx  16066  upgrex  16090  subumgredg2en  16258  iedginwlk  16344  eulerpathprum  16467  gfsumsn  16858