Theorem simp1 949

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

Syntax hints:   → wi 4   ∧ w3a 930

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-3an 932

This theorem is referenced by:  simpl1  952  simpr1  955  simp1i  958  simp1d  961  simp11  979  simp21  982  simp31  985  syld3an3  1229  3ianorr  1255  stoic4a  1376  stoic4b  1377  rsp2e  2442  issod  4179  elirr  4394  sotri2  4872  sotri3  4873  funtpg  5110  funimaexglem  5142  feq123  5200  ftpg  5536  fsnunf  5552  foco2  5587  fcofo  5617  f1oiso2  5660  riotass  5689  ovmpox  5831  ovmpoga  5832  caovimo  5896  ofeq  5916  ofrval  5924  tfr1onlembxssdm  6170  tfrcllembxssdm  6183  frecsuclem  6233  frecrdg  6235  mapxpen  6671  diffifi  6717  unsnfidcex  6737  unsnfidcel  6738  unfidisj  6739  undifdc  6741  ssfidc  6751  iunfidisj  6762  sbthlemi9  6781  djuassen  6977  mulcanenq  7094  ltanqg  7109  addnnnq0  7158  distrlem4prl  7293  distrlem4pru  7294  distrprg  7297  aptipr  7350  addsrpr  7441  mulsrpr  7442  mulasssrg  7454  axmulass  7558  axpre-ltadd  7571  mul31  7764  addsubass  7843  subcan2  7858  subsub2  7861  subsub4  7866  npncan3  7871  pnpcan  7872  pnncan  7874  subcan  7888  subdi  8014  ltadd1  8058  leadd1  8059  leadd2  8060  ltsubadd  8061  lesubadd  8063  ltaddsub  8065  leaddsub  8067  lesub1  8085  lesub2  8086  ltsub1  8087  ltsub2  8088  ltaddsublt  8199  gt0add  8201  apreap  8215  lemul1  8221  reapmul1lem  8222  reapmul1  8223  reapadd1  8224  remulext1  8227  remulext2  8228  apadd2  8237  mulext2  8241  mulap0r  8243  leltap  8253  ltap  8260  apsub1  8269  recexaplem2  8274  mulcanap  8287  mulcanap2  8288  divvalap  8295  divcanap2  8301  diveqap0  8303  divrecap  8309  divrecap2  8310  divdirap  8318  divcanap3  8319  div11ap  8321  muldivdirap  8328  divcanap5  8335  redivclap  8352  div2negap  8356  apmul1  8409  apmul2  8410  div2subap  8457  ltdiv1  8484  ltmuldiv  8490  lemuldiv  8497  lt2msq1  8501  ltdiv23  8508  lediv23  8509  squeeze0  8520  gtndiv  8998  eluz2  9182  eluzsub  9205  peano2uz  9228  nn01to3  9259  divge1  9357  ledivge1le  9360  addlelt  9396  xaddass  9493  xleadd1  9499  xltadd1  9500  ixxssixx  9526  lbico1  9554  lbicc2  9608  icoshftf1o  9615  fzen  9664  fzrev3  9708  fzrevral2  9727  elfzo0  9800  elfzo0z  9802  fzosplitprm1  9852  qbtwnre  9875  flqwordi  9902  flqword2  9903  adddivflid  9906  flltdivnn0lt  9918  modqcl  9940  mulqmod0  9944  modqmulnn  9956  modqabs2  9972  addmodid  9986  modifeq2int  10000  modqeqmodmin  10008  seqeq2  10063  seqeq3  10064  exp3val  10136  expnegap0  10142  expgt1  10172  exprecap  10175  leexp2a  10187  expubnd  10191  sqdivap  10198  expnbnd  10256  bccmpl  10341  fihashss  10403  leisorel  10421  shftfibg  10433  mulreap  10477  abssubne0  10703  maxleast  10825  lemininf  10844  ltmininf  10845  xrmaxltsup  10866  xrmaxaddlem  10868  xrmaxadd  10869  xrmineqinf  10877  xrltmininf  10878  xrminltinf  10880  xrminadd  10883  climuni  10901  reccn2ap  10921  isumz  10997  fsumsplitsnun  11027  geoisum1c  11128  efltim  11202  dvdscmulr  11317  dvdsmulcr  11318  summodnegmod  11319  modmulconst  11320  dvdsmultr2  11328  dvdsexp  11354  mulmoddvds  11356  modremain  11421  divgcdz  11455  gcdaddm  11467  dvdsgcdb  11494  gcdass  11496  mulgcd  11497  gcddiv  11500  rplpwr  11508  lcmdvdsb  11558  lcmass  11559  mulgcddvds  11568  qredeq  11570  qredeu  11571  rpmul  11572  divgcdcoprmex  11576  cncongr1  11577  rpexp  11624  rpexp12i  11626  ctinf  11735  setsvala  11772  ressid2  11800  ressval2  11801  rngbaseg  11857  2basgeng  12033  clsss  12069  ntrss  12070  ntrin  12075  neiss  12101  restco  12125  restabs  12126  lmconst  12166  psmetsym  12257  psmetge0  12259  xmetge0  12293  xmetsym  12296  xmetresbl  12368  mopni3  12412  bdxmet  12429  bdmopn  12432  dvfvalap  12523  dvid  12535