Theorem simp1 997

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  simpl1  1000  simpr1  1003  simp1i  1006  simp1d  1009  simp11  1027  simp21  1030  simp31  1033  syld3an3  1283  3ianorr  1309  stoic4a  1432  stoic4b  1433  rsp2e  2528  issod  4319  elirr  4540  sotri2  5026  sotri3  5027  funtpg  5267  funimaexglem  5299  feq123  5357  ftpg  5700  fsnunf  5716  foco2  5754  fcofo  5784  f1oiso2  5827  riotass  5857  ovmpox  6002  ovmpoga  6003  caovimo  6067  ofeq  6084  ofrval  6092  tfr1onlembxssdm  6343  tfrcllembxssdm  6356  frecsuclem  6406  frecrdg  6408  mapxpen  6847  diffifi  6893  unsnfidcex  6918  unsnfidcel  6919  unfidisj  6920  undifdc  6922  ssfidc  6933  iunfidisj  6944  sbthlemi9  6963  elfir  6971  djuassen  7215  dftap2  7249  mulcanenq  7383  ltanqg  7398  addnnnq0  7447  distrlem4prl  7582  distrlem4pru  7583  distrprg  7586  aptipr  7639  addsrpr  7743  mulsrpr  7744  mulasssrg  7756  ltpsrprg  7801  axmulass  7871  axpre-ltadd  7884  mul31  8087  addsubass  8166  subcan2  8181  subsub2  8184  subsub4  8189  npncan3  8194  pnpcan  8195  pnncan  8197  subcan  8211  subdi  8341  ltadd1  8385  leadd1  8386  leadd2  8387  ltsubadd  8388  lesubadd  8390  ltaddsub  8392  leaddsub  8394  lesub1  8412  lesub2  8413  ltsub1  8414  ltsub2  8415  ltaddsublt  8527  gt0add  8529  apreap  8543  lemul1  8549  reapmul1lem  8550  reapmul1  8551  reapadd1  8552  remulext1  8555  remulext2  8556  apadd2  8565  mulext2  8569  mulap0r  8571  leltap  8581  ltap  8589  apsub1  8598  recexaplem2  8608  mulcanap  8621  mulcanap2  8622  divvalap  8630  divcanap2  8636  diveqap0  8638  divrecap  8644  divrecap2  8645  divdirap  8653  divcanap3  8654  div11ap  8656  muldivdirap  8663  divcanap5  8670  redivclap  8687  div2negap  8691  apmul1  8744  apmul2  8745  div2subap  8793  ltdiv1  8824  ltmuldiv  8830  lemuldiv  8837  lt2msq1  8841  ltdiv23  8848  lediv23  8849  squeeze0  8860  difgtsumgt  9321  gtndiv  9347  eluz2  9533  eluzsub  9556  peano2uz  9582  nn01to3  9616  divge1  9722  ledivge1le  9725  addlelt  9767  xaddass  9868  xleadd1  9874  xltadd1  9875  ixxssixx  9901  lbico1  9929  lbicc2  9983  icoshftf1o  9990  fzen  10042  fzrev3  10086  fzrevral2  10105  elfzo0  10181  elfzo0z  10183  fzosplitprm1  10233  qbtwnre  10256  flqwordi  10287  flqword2  10288  adddivflid  10291  flltdivnn0lt  10303  modqcl  10325  mulqmod0  10329  modqmulnn  10341  modqabs2  10357  addmodid  10371  modifeq2int  10385  modqeqmodmin  10393  seqeq2  10448  seqeq3  10449  exp3val  10521  expnegap0  10527  expgt1  10557  exprecap  10560  leexp2a  10572  expubnd  10576  sqdivap  10583  expnbnd  10643  mulsubdivbinom2ap  10690  bccmpl  10733  fihashss  10795  leisorel  10816  shftfibg  10828  mulreap  10872  abssubne0  11099  maxleast  11221  lemininf  11241  ltmininf  11242  xrmaxltsup  11265  xrmaxaddlem  11267  xrmaxadd  11268  xrmineqinf  11276  xrltmininf  11277  xrminltinf  11279  xrminadd  11282  climuni  11300  reccn2ap  11320  isumz  11396  fsumsplitsnun  11426  geoisum1c  11527  prod1dc  11593  efltim  11705  dvdscmulr  11826  dvdsmulcr  11827  summodnegmod  11828  modmulconst  11829  dvdsmultr2  11839  dvdsexp  11866  mulmoddvds  11868  modremain  11933  divgcdz  11971  gcdaddm  11984  dvdsgcdb  12013  gcdass  12015  mulgcd  12016  gcddiv  12019  rplpwr  12027  uzwodc  12037  lcmdvdsb  12083  lcmass  12084  mulgcddvds  12093  qredeq  12095  qredeu  12096  rpmul  12097  divgcdcoprmex  12101  cncongr1  12102  rpexp  12152  rpexp12i  12154  odzcllem  12241  odzdvds  12244  odzphi  12245  pythagtriplem15  12277  pcpremul  12292  pcdiv  12301  pcqmul  12302  pcqdiv  12306  dvdsprmpweq  12333  sumhashdc  12344  pcfaclem  12346  qexpz  12349  ctinf  12430  setsvala  12492  ressressg  12533  ressabsg  12534  rngbaseg  12593  ptex  12712  issubmnd  12842  ress0g  12843  grpasscan2  12933  grpidrcan  12934  grpidlcan  12935  grpinvadd  12947  grpsubeq0  12955  grppncan  12960  dfgrp3m  12968  grpsubpropd2  12974  mhmmnd  12979  mulgnegneg  13001  mulgaddcomlem  13004  mulgaddcom  13005  mulginvcom  13006  mulgmodid  13020  issubg  13031  nsgconj  13064  nsgid  13073  cmn4  13106  ablinvadd  13111  ablsub4  13114  abladdsub4  13115  ablpncan2  13117  issrg  13146  ringidss  13210  ringcom  13212  unitmulcl  13280  unitmulclb  13281  dvrcl  13302  unitdvcl  13303  dvrcan1  13307  dvrcan3  13308  islmod  13379  2basgeng  13552  clsss  13588  ntrss  13589  ntrin  13594  neiss  13620  restco  13644  restabs  13645  lmconst  13686  psmetsym  13799  psmetge0  13801  xmetge0  13835  xmetsym  13838  xmetresbl  13910  mopni3  13954  bdxmet  13971  bdmopn  13974  txmetcnp  13988  dvfvalap  14120  dvid  14132  dvcnp2cntop  14133  ptolemy  14215  rpcxpadd  14296  rpmulcxp  14300  rpdivcxp  14302  cxpmul  14303  rpcxple2  14308  rpcxplt2  14309  cxpcom  14327  rplogbval  14333  rplogbcl  14334  rprelogbmulexp  14344  relogbexpap  14346  logbleb  14349  logblt  14350  rplogbcxp  14351  rpcxplogb  14352  lgslem1  14371  lgsfcl2  14377  lgsneg  14395  lgsne0  14409  lgssq2  14412  lgsdirnn0  14418  2lgsoddprmlem2  14424