Theorem simp1 981

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

Syntax hints:   → wi 4   ∧ w3a 962

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

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

This theorem is referenced by:  simpl1  984  simpr1  987  simp1i  990  simp1d  993  simp11  1011  simp21  1014  simp31  1017  syld3an3  1261  3ianorr  1287  stoic4a  1408  stoic4b  1409  rsp2e  2481  issod  4236  elirr  4451  sotri2  4931  sotri3  4932  funtpg  5169  funimaexglem  5201  feq123  5259  ftpg  5597  fsnunf  5613  foco2  5648  fcofo  5678  f1oiso2  5721  riotass  5750  ovmpox  5892  ovmpoga  5893  caovimo  5957  ofeq  5977  ofrval  5985  tfr1onlembxssdm  6233  tfrcllembxssdm  6246  frecsuclem  6296  frecrdg  6298  mapxpen  6735  diffifi  6781  unsnfidcex  6801  unsnfidcel  6802  unfidisj  6803  undifdc  6805  ssfidc  6816  iunfidisj  6827  sbthlemi9  6846  elfir  6854  djuassen  7066  mulcanenq  7186  ltanqg  7201  addnnnq0  7250  distrlem4prl  7385  distrlem4pru  7386  distrprg  7389  aptipr  7442  addsrpr  7546  mulsrpr  7547  mulasssrg  7559  ltpsrprg  7604  axmulass  7674  axpre-ltadd  7687  mul31  7886  addsubass  7965  subcan2  7980  subsub2  7983  subsub4  7988  npncan3  7993  pnpcan  7994  pnncan  7996  subcan  8010  subdi  8140  ltadd1  8184  leadd1  8185  leadd2  8186  ltsubadd  8187  lesubadd  8189  ltaddsub  8191  leaddsub  8193  lesub1  8211  lesub2  8212  ltsub1  8213  ltsub2  8214  ltaddsublt  8326  gt0add  8328  apreap  8342  lemul1  8348  reapmul1lem  8349  reapmul1  8350  reapadd1  8351  remulext1  8354  remulext2  8355  apadd2  8364  mulext2  8368  mulap0r  8370  leltap  8380  ltap  8388  apsub1  8397  recexaplem2  8406  mulcanap  8419  mulcanap2  8420  divvalap  8427  divcanap2  8433  diveqap0  8435  divrecap  8441  divrecap2  8442  divdirap  8450  divcanap3  8451  div11ap  8453  muldivdirap  8460  divcanap5  8467  redivclap  8484  div2negap  8488  apmul1  8541  apmul2  8542  div2subap  8589  ltdiv1  8619  ltmuldiv  8625  lemuldiv  8632  lt2msq1  8636  ltdiv23  8643  lediv23  8644  squeeze0  8655  gtndiv  9139  eluz2  9325  eluzsub  9348  peano2uz  9371  nn01to3  9402  divge1  9503  ledivge1le  9506  addlelt  9548  xaddass  9645  xleadd1  9651  xltadd1  9652  ixxssixx  9678  lbico1  9706  lbicc2  9760  icoshftf1o  9767  fzen  9816  fzrev3  9860  fzrevral2  9879  elfzo0  9952  elfzo0z  9954  fzosplitprm1  10004  qbtwnre  10027  flqwordi  10054  flqword2  10055  adddivflid  10058  flltdivnn0lt  10070  modqcl  10092  mulqmod0  10096  modqmulnn  10108  modqabs2  10124  addmodid  10138  modifeq2int  10152  modqeqmodmin  10160  seqeq2  10215  seqeq3  10216  exp3val  10288  expnegap0  10294  expgt1  10324  exprecap  10327  leexp2a  10339  expubnd  10343  sqdivap  10350  expnbnd  10408  bccmpl  10493  fihashss  10555  leisorel  10573  shftfibg  10585  mulreap  10629  abssubne0  10856  maxleast  10978  lemininf  10998  ltmininf  10999  xrmaxltsup  11020  xrmaxaddlem  11022  xrmaxadd  11023  xrmineqinf  11031  xrltmininf  11032  xrminltinf  11034  xrminadd  11037  climuni  11055  reccn2ap  11075  isumz  11151  fsumsplitsnun  11181  geoisum1c  11282  efltim  11393  dvdscmulr  11511  dvdsmulcr  11512  summodnegmod  11513  modmulconst  11514  dvdsmultr2  11522  dvdsexp  11548  mulmoddvds  11550  modremain  11615  divgcdz  11649  gcdaddm  11661  dvdsgcdb  11690  gcdass  11692  mulgcd  11693  gcddiv  11696  rplpwr  11704  lcmdvdsb  11754  lcmass  11755  mulgcddvds  11764  qredeq  11766  qredeu  11767  rpmul  11768  divgcdcoprmex  11772  cncongr1  11773  rpexp  11820  rpexp12i  11822  ctinf  11932  setsvala  11979  ressid2  12007  ressval2  12008  rngbaseg  12064  2basgeng  12240  clsss  12276  ntrss  12277  ntrin  12282  neiss  12308  restco  12332  restabs  12333  lmconst  12374  psmetsym  12487  psmetge0  12489  xmetge0  12523  xmetsym  12526  xmetresbl  12598  mopni3  12642  bdxmet  12659  bdmopn  12662  txmetcnp  12676  dvfvalap  12808  dvid  12820  dvcnp2cntop  12821  ptolemy  12894