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  5400  ftpg  5747  fsnunf  5763  foco2  5801  fcofo  5832  f1oiso2  5875  riotass  5906  ovmpox  6053  ovmpoga  6054  caovimo  6119  ofeq  6140  ofrval  6148  tfr1onlembxssdm  6403  tfrcllembxssdm  6416  frecsuclem  6466  frecrdg  6468  mapxpen  6911  diffifi  6957  unsnfidcex  6983  unsnfidcel  6984  unfidisj  6985  undifdc  6987  ssfidc  7000  iunfidisj  7014  sbthlemi9  7033  elfir  7041  djuassen  7287  dftap2  7321  mulcanenq  7455  ltanqg  7470  addnnnq0  7519  distrlem4prl  7654  distrlem4pru  7655  distrprg  7658  aptipr  7711  addsrpr  7815  mulsrpr  7816  mulasssrg  7828  ltpsrprg  7873  axmulass  7943  axpre-ltadd  7956  mul31  8160  addsubass  8239  subcan2  8254  subsub2  8257  subsub4  8262  npncan3  8267  pnpcan  8268  pnncan  8270  subcan  8284  subdi  8414  ltadd1  8459  leadd1  8460  leadd2  8461  ltsubadd  8462  lesubadd  8464  ltaddsub  8466  leaddsub  8468  lesub1  8486  lesub2  8487  ltsub1  8488  ltsub2  8489  ltaddsublt  8601  gt0add  8603  apreap  8617  lemul1  8623  reapmul1lem  8624  reapmul1  8625  reapadd1  8626  remulext1  8629  remulext2  8630  apadd2  8639  mulext2  8643  mulap0r  8645  leltap  8655  ltap  8663  apsub1  8672  recexaplem2  8682  mulcanap  8695  mulcanap2  8696  divvalap  8704  divcanap2  8710  diveqap0  8712  divrecap  8718  divrecap2  8719  divdirap  8727  divcanap3  8728  div11ap  8730  muldivdirap  8737  divcanap5  8744  redivclap  8761  div2negap  8765  apmul1  8818  apmul2  8819  div2subap  8867  ltdiv1  8898  ltmuldiv  8904  lemuldiv  8911  lt2msq1  8915  ltdiv23  8922  lediv23  8923  squeeze0  8934  ofnegsub  8992  difgtsumgt  9398  gtndiv  9424  eluz2  9610  eluzsub  9634  peano2uz  9660  nn01to3  9694  divge1  9801  ledivge1le  9804  addlelt  9846  xaddass  9947  xleadd1  9953  xltadd1  9954  ixxssixx  9980  lbico1  10008  lbicc2  10062  icoshftf1o  10069  fzen  10121  fzrev3  10165  fzrevral2  10184  nelfzo  10230  elfzo0  10261  elfzo0z  10263  fzosplitprm1  10313  qbtwnre  10349  flqwordi  10381  flqword2  10382  adddivflid  10385  flltdivnn0lt  10397  modqcl  10421  mulqmod0  10425  modqmulnn  10437  modqabs2  10453  addmodid  10467  modifeq2int  10481  modqeqmodmin  10489  seqeq2  10546  seqeq3  10547  seq1g  10558  seqp1g  10561  exp3val  10636  expnegap0  10642  expgt1  10672  exprecap  10675  leexp2a  10687  expubnd  10691  sqdivap  10698  expnbnd  10758  mulsubdivbinom2ap  10806  bccmpl  10849  fihashss  10911  leisorel  10932  shftfibg  10988  mulreap  11032  abssubne0  11259  maxleast  11381  lemininf  11402  ltmininf  11403  xrmaxltsup  11426  xrmaxaddlem  11428  xrmaxadd  11429  xrmineqinf  11437  xrltmininf  11438  xrminltinf  11440  xrminadd  11443  climuni  11461  reccn2ap  11481  isumz  11557  fsumsplitsnun  11587  geoisum1c  11688  prod1dc  11754  efltim  11866  dvdscmulr  11988  dvdsmulcr  11989  summodnegmod  11990  modmulconst  11991  dvdsmultr2  12001  dvdsexp  12029  mulmoddvds  12031  modremain  12097  divgcdz  12149  gcdaddm  12162  dvdsgcdb  12191  gcdass  12193  mulgcd  12194  gcddiv  12197  rplpwr  12205  uzwodc  12215  lcmdvdsb  12263  lcmass  12264  mulgcddvds  12273  qredeq  12275  qredeu  12276  rpmul  12277  divgcdcoprmex  12281  cncongr1  12282  rpexp  12332  rpexp12i  12334  odzcllem  12422  odzdvds  12425  odzphi  12426  pythagtriplem15  12458  pcpremul  12473  pcdiv  12482  pcqmul  12483  pcqdiv  12487  dvdsprmpweq  12515  sumhashdc  12527  pcfaclem  12529  qexpz  12532  ctinf  12658  setsvala  12720  ressressg  12764  ressabsg  12765  rngbaseg  12824  ptex  12952  issubmnd  13109  ress0g  13110  gsumfzz  13153  grpasscan2  13222  grpidrcan  13223  grpidlcan  13224  grpinvadd  13236  grpsubeq0  13244  grppncan  13249  dfgrp3m  13257  grpsubpropd2  13263  imasgrp2  13266  mhmmnd  13272  mulgnegneg  13297  mulgaddcomlem  13301  mulgaddcom  13302  mulginvcom  13303  mulgmodid  13317  issubg  13329  nsgconj  13362  nsgid  13371  quselbasg  13386  quseccl0g  13387  ghmnsgima  13424  cmn4  13461  ablinvadd  13466  ablsub4  13469  abladdsub4  13470  ablpncan2  13472  rngpropd  13537  imasrng  13538  issrg  13547  ringidss  13611  ringcom  13613  imasring  13646  unitmulcl  13695  unitmulclb  13696  dvrcl  13717  unitdvcl  13718  dvrcan1  13722  dvrcan3  13723  issubrng  13781  subrngpropd  13798  rrgeq0  13847  islmod  13873  lmodcom  13915  rmodislmodlem  13932  rmodislmod  13933  lss0cl  13951  lssvnegcl  13958  lssintclm  13966  lssincl  13967  lspss  13981  lspun  13984  lspsnvsi  14000  lsslsp  14011  rnglidlmmgm  14078  rnglidlmsgrp  14079  rnglidlrng  14080  qus2idrng  14107  qusmulrng  14114  2basgeng  14344  clsss  14380  ntrss  14381  ntrin  14386  neiss  14412  restco  14436  restabs  14437  lmconst  14478  psmetsym  14591  psmetge0  14593  xmetge0  14627  xmetsym  14630  xmetresbl  14702  mopni3  14746  bdxmet  14763  bdmopn  14766  txmetcnp  14780  dvfvalap  14943  dvid  14957  dvidre  14959  dvcnp2cntop  14961  elplyr  15002  ply1term  15005  ptolemy  15086  rpcxpadd  15167  rpmulcxp  15171  rpdivcxp  15173  cxpmul  15174  rpcxple2  15180  rpcxplt2  15181  cxpcom  15200  rplogbval  15207  rplogbcl  15208  rprelogbmulexp  15218  relogbexpap  15220  logbleb  15223  logblt  15224  rplogbcxp  15225  rpcxplogb  15226  sgmppw  15254  lgslem1  15267  lgsfcl2  15273  lgsneg  15291  lgsne0  15305  lgssq2  15308  lgsdirnn0  15314  gausslemma2dlem1a  15325  lgsquad  15347  2lgsoddprmlem2  15373