Theorem simp1 999

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simpl1  1002  simpr1  1005  simp1i  1008  simp1d  1011  simp11  1029  simp21  1032  simp31  1035  syld3an3  1294  3ianorr  1320  stoic4a  1443  stoic4b  1444  rsp2e  2548  ifnetruedc  3603  issod  4355  elirr  4578  sotri2  5068  sotri3  5069  funtpg  5310  funimaexglem  5342  feq123  5402  ftpg  5749  fsnunf  5765  foco2  5803  fcofo  5834  f1oiso2  5877  riotass  5908  ovmpox  6055  ovmpoga  6056  caovimo  6121  ofeq  6142  ofrval  6150  tfr1onlembxssdm  6410  tfrcllembxssdm  6423  frecsuclem  6473  frecrdg  6475  mapxpen  6918  diffifi  6964  unsnfidcex  6990  unsnfidcel  6991  unfidisj  6992  undifdc  6994  ssfidc  7007  iunfidisj  7021  sbthlemi9  7040  elfir  7048  djuassen  7300  dftap2  7334  mulcanenq  7469  ltanqg  7484  addnnnq0  7533  distrlem4prl  7668  distrlem4pru  7669  distrprg  7672  aptipr  7725  addsrpr  7829  mulsrpr  7830  mulasssrg  7842  ltpsrprg  7887  axmulass  7957  axpre-ltadd  7970  mul31  8174  addsubass  8253  subcan2  8268  subsub2  8271  subsub4  8276  npncan3  8281  pnpcan  8282  pnncan  8284  subcan  8298  subdi  8428  ltadd1  8473  leadd1  8474  leadd2  8475  ltsubadd  8476  lesubadd  8478  ltaddsub  8480  leaddsub  8482  lesub1  8500  lesub2  8501  ltsub1  8502  ltsub2  8503  ltaddsublt  8615  gt0add  8617  apreap  8631  lemul1  8637  reapmul1lem  8638  reapmul1  8639  reapadd1  8640  remulext1  8643  remulext2  8644  apadd2  8653  mulext2  8657  mulap0r  8659  leltap  8669  ltap  8677  apsub1  8686  recexaplem2  8696  mulcanap  8709  mulcanap2  8710  divvalap  8718  divcanap2  8724  diveqap0  8726  divrecap  8732  divrecap2  8733  divdirap  8741  divcanap3  8742  div11ap  8744  muldivdirap  8751  divcanap5  8758  redivclap  8775  div2negap  8779  apmul1  8832  apmul2  8833  div2subap  8881  ltdiv1  8912  ltmuldiv  8918  lemuldiv  8925  lt2msq1  8929  ltdiv23  8936  lediv23  8937  squeeze0  8948  ofnegsub  9006  difgtsumgt  9412  gtndiv  9438  eluz2  9624  eluzsub  9648  peano2uz  9674  nn01to3  9708  divge1  9815  ledivge1le  9818  addlelt  9860  xaddass  9961  xleadd1  9967  xltadd1  9968  ixxssixx  9994  lbico1  10022  lbicc2  10076  icoshftf1o  10083  fzen  10135  fzrev3  10179  fzrevral2  10198  nelfzo  10244  elfzo0  10275  elfzo0z  10277  fzosplitprm1  10327  qbtwnre  10363  flqwordi  10395  flqword2  10396  adddivflid  10399  flltdivnn0lt  10411  modqcl  10435  mulqmod0  10439  modqmulnn  10451  modqabs2  10467  addmodid  10481  modifeq2int  10495  modqeqmodmin  10503  seqeq2  10560  seqeq3  10561  seq1g  10572  seqp1g  10575  exp3val  10650  expnegap0  10656  expgt1  10686  exprecap  10689  leexp2a  10701  expubnd  10705  sqdivap  10712  expnbnd  10772  mulsubdivbinom2ap  10820  bccmpl  10863  fihashss  10925  leisorel  10946  shftfibg  11002  mulreap  11046  abssubne0  11273  maxleast  11395  lemininf  11416  ltmininf  11417  xrmaxltsup  11440  xrmaxaddlem  11442  xrmaxadd  11443  xrmineqinf  11451  xrltmininf  11452  xrminltinf  11454  xrminadd  11457  climuni  11475  reccn2ap  11495  isumz  11571  fsumsplitsnun  11601  geoisum1c  11702  prod1dc  11768  efltim  11880  dvdscmulr  12002  dvdsmulcr  12003  summodnegmod  12004  modmulconst  12005  dvdsmultr2  12015  dvdsexp  12043  mulmoddvds  12045  modremain  12111  divgcdz  12163  gcdaddm  12176  dvdsgcdb  12205  gcdass  12207  mulgcd  12208  gcddiv  12211  rplpwr  12219  uzwodc  12229  lcmdvdsb  12277  lcmass  12278  mulgcddvds  12287  qredeq  12289  qredeu  12290  rpmul  12291  divgcdcoprmex  12295  cncongr1  12296  rpexp  12346  rpexp12i  12348  odzcllem  12436  odzdvds  12439  odzphi  12440  pythagtriplem15  12472  pcpremul  12487  pcdiv  12496  pcqmul  12497  pcqdiv  12501  dvdsprmpweq  12529  sumhashdc  12541  pcfaclem  12543  qexpz  12546  ctinf  12672  setsvala  12734  ressressg  12778  ressabsg  12779  rngbaseg  12838  ptex  12966  issubmnd  13144  ress0g  13145  imasmnd2  13154  gsumfzz  13197  grpasscan2  13266  grpidrcan  13267  grpidlcan  13268  grpinvadd  13280  grpsubeq0  13288  grppncan  13293  dfgrp3m  13301  grpsubpropd2  13307  pwsinvg  13314  imasgrp2  13316  mhmmnd  13322  mulgnegneg  13347  mulgaddcomlem  13351  mulgaddcom  13352  mulginvcom  13353  mulgmodid  13367  issubg  13379  nsgconj  13412  nsgid  13421  quselbasg  13436  quseccl0g  13437  ghmnsgima  13474  cmn4  13511  ablinvadd  13516  ablsub4  13519  abladdsub4  13520  ablpncan2  13522  rngpropd  13587  imasrng  13588  issrg  13597  ringidss  13661  ringcom  13663  imasring  13696  unitmulcl  13745  unitmulclb  13746  dvrcl  13767  unitdvcl  13768  dvrcan1  13772  dvrcan3  13773  issubrng  13831  subrngpropd  13848  rrgeq0  13897  islmod  13923  lmodcom  13965  rmodislmodlem  13982  rmodislmod  13983  lss0cl  14001  lssvnegcl  14008  lssintclm  14016  lssincl  14017  lspss  14031  lspun  14034  lspsnvsi  14050  lsslsp  14061  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  qus2idrng  14157  qusmulrng  14164  2basgeng  14402  clsss  14438  ntrss  14439  ntrin  14444  neiss  14470  restco  14494  restabs  14495  lmconst  14536  psmetsym  14649  psmetge0  14651  xmetge0  14685  xmetsym  14688  xmetresbl  14760  mopni3  14804  bdxmet  14821  bdmopn  14824  txmetcnp  14838  dvfvalap  15001  dvid  15015  dvidre  15017  dvcnp2cntop  15019  elplyr  15060  ply1term  15063  ptolemy  15144  rpcxpadd  15225  rpmulcxp  15229  rpdivcxp  15231  cxpmul  15232  rpcxple2  15238  rpcxplt2  15239  cxpcom  15258  rplogbval  15265  rplogbcl  15266  rprelogbmulexp  15276  relogbexpap  15278  logbleb  15281  logblt  15282  rplogbcxp  15283  rpcxplogb  15284  sgmppw  15312  lgslem1  15325  lgsfcl2  15331  lgsneg  15349  lgsne0  15363  lgssq2  15366  lgsdirnn0  15372  gausslemma2dlem1a  15383  lgsquad  15405  2lgsoddprmlem2  15431