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  2541  issod  4337  elirr  4558  sotri2  5044  sotri3  5045  funtpg  5286  funimaexglem  5318  feq123  5376  ftpg  5721  fsnunf  5737  foco2  5775  fcofo  5806  f1oiso2  5849  riotass  5880  ovmpox  6026  ovmpoga  6027  caovimo  6091  ofeq  6110  ofrval  6118  tfr1onlembxssdm  6369  tfrcllembxssdm  6382  frecsuclem  6432  frecrdg  6434  mapxpen  6877  diffifi  6923  unsnfidcex  6949  unsnfidcel  6950  unfidisj  6951  undifdc  6953  ssfidc  6964  iunfidisj  6976  sbthlemi9  6995  elfir  7003  djuassen  7247  dftap2  7281  mulcanenq  7415  ltanqg  7430  addnnnq0  7479  distrlem4prl  7614  distrlem4pru  7615  distrprg  7618  aptipr  7671  addsrpr  7775  mulsrpr  7776  mulasssrg  7788  ltpsrprg  7833  axmulass  7903  axpre-ltadd  7916  mul31  8119  addsubass  8198  subcan2  8213  subsub2  8216  subsub4  8221  npncan3  8226  pnpcan  8227  pnncan  8229  subcan  8243  subdi  8373  ltadd1  8417  leadd1  8418  leadd2  8419  ltsubadd  8420  lesubadd  8422  ltaddsub  8424  leaddsub  8426  lesub1  8444  lesub2  8445  ltsub1  8446  ltsub2  8447  ltaddsublt  8559  gt0add  8561  apreap  8575  lemul1  8581  reapmul1lem  8582  reapmul1  8583  reapadd1  8584  remulext1  8587  remulext2  8588  apadd2  8597  mulext2  8601  mulap0r  8603  leltap  8613  ltap  8621  apsub1  8630  recexaplem2  8640  mulcanap  8653  mulcanap2  8654  divvalap  8662  divcanap2  8668  diveqap0  8670  divrecap  8676  divrecap2  8677  divdirap  8685  divcanap3  8686  div11ap  8688  muldivdirap  8695  divcanap5  8702  redivclap  8719  div2negap  8723  apmul1  8776  apmul2  8777  div2subap  8825  ltdiv1  8856  ltmuldiv  8862  lemuldiv  8869  lt2msq1  8873  ltdiv23  8880  lediv23  8881  squeeze0  8892  difgtsumgt  9353  gtndiv  9379  eluz2  9565  eluzsub  9589  peano2uz  9615  nn01to3  9649  divge1  9755  ledivge1le  9758  addlelt  9800  xaddass  9901  xleadd1  9907  xltadd1  9908  ixxssixx  9934  lbico1  9962  lbicc2  10016  icoshftf1o  10023  fzen  10075  fzrev3  10119  fzrevral2  10138  elfzo0  10214  elfzo0z  10216  fzosplitprm1  10266  qbtwnre  10289  flqwordi  10321  flqword2  10322  adddivflid  10325  flltdivnn0lt  10337  modqcl  10359  mulqmod0  10363  modqmulnn  10375  modqabs2  10391  addmodid  10405  modifeq2int  10419  modqeqmodmin  10427  seqeq2  10482  seqeq3  10483  exp3val  10556  expnegap0  10562  expgt1  10592  exprecap  10595  leexp2a  10607  expubnd  10611  sqdivap  10618  expnbnd  10678  mulsubdivbinom2ap  10726  bccmpl  10769  fihashss  10831  leisorel  10852  shftfibg  10864  mulreap  10908  abssubne0  11135  maxleast  11257  lemininf  11277  ltmininf  11278  xrmaxltsup  11301  xrmaxaddlem  11303  xrmaxadd  11304  xrmineqinf  11312  xrltmininf  11313  xrminltinf  11315  xrminadd  11318  climuni  11336  reccn2ap  11356  isumz  11432  fsumsplitsnun  11462  geoisum1c  11563  prod1dc  11629  efltim  11741  dvdscmulr  11862  dvdsmulcr  11863  summodnegmod  11864  modmulconst  11865  dvdsmultr2  11875  dvdsexp  11902  mulmoddvds  11904  modremain  11969  divgcdz  12007  gcdaddm  12020  dvdsgcdb  12049  gcdass  12051  mulgcd  12052  gcddiv  12055  rplpwr  12063  uzwodc  12073  lcmdvdsb  12119  lcmass  12120  mulgcddvds  12129  qredeq  12131  qredeu  12132  rpmul  12133  divgcdcoprmex  12137  cncongr1  12138  rpexp  12188  rpexp12i  12190  odzcllem  12277  odzdvds  12280  odzphi  12281  pythagtriplem15  12313  pcpremul  12328  pcdiv  12337  pcqmul  12338  pcqdiv  12342  dvdsprmpweq  12370  sumhashdc  12382  pcfaclem  12384  qexpz  12387  ctinf  12484  setsvala  12546  ressressg  12590  ressabsg  12591  rngbaseg  12650  ptex  12772  issubmnd  12918  ress0g  12919  grpasscan2  13023  grpidrcan  13024  grpidlcan  13025  grpinvadd  13037  grpsubeq0  13045  grppncan  13050  dfgrp3m  13058  grpsubpropd2  13064  imasgrp2  13067  mhmmnd  13073  mulgnegneg  13098  mulgaddcomlem  13102  mulgaddcom  13103  mulginvcom  13104  mulgmodid  13118  issubg  13129  nsgconj  13162  nsgid  13171  quselbasg  13186  quseccl0g  13187  ghmnsgima  13224  cmn4  13261  ablinvadd  13266  ablsub4  13269  abladdsub4  13270  ablpncan2  13272  rngpropd  13326  imasrng  13327  issrg  13336  ringidss  13400  ringcom  13402  imasring  13431  unitmulcl  13480  unitmulclb  13481  dvrcl  13502  unitdvcl  13503  dvrcan1  13507  dvrcan3  13508  issubrng  13563  subrngpropd  13580  islmod  13624  lmodcom  13666  rmodislmodlem  13683  rmodislmod  13684  lss0cl  13702  lssvnegcl  13709  lssintclm  13717  lssincl  13718  lspss  13732  lspun  13735  lspsnvsi  13751  lsslsp  13762  rnglidlmmgm  13829  rnglidlmsgrp  13830  rnglidlrng  13831  qus2idrng  13857  qusmulrng  13863  2basgeng  14059  clsss  14095  ntrss  14096  ntrin  14101  neiss  14127  restco  14151  restabs  14152  lmconst  14193  psmetsym  14306  psmetge0  14308  xmetge0  14342  xmetsym  14345  xmetresbl  14417  mopni3  14461  bdxmet  14478  bdmopn  14481  txmetcnp  14495  dvfvalap  14627  dvid  14639  dvcnp2cntop  14640  ptolemy  14722  rpcxpadd  14803  rpmulcxp  14807  rpdivcxp  14809  cxpmul  14810  rpcxple2  14815  rpcxplt2  14816  cxpcom  14834  rplogbval  14840  rplogbcl  14841  rprelogbmulexp  14851  relogbexpap  14853  logbleb  14856  logblt  14857  rplogbcxp  14858  rpcxplogb  14859  lgslem1  14879  lgsfcl2  14885  lgsneg  14903  lgsne0  14917  lgssq2  14920  lgsdirnn0  14926  2lgsoddprmlem2  14932