Theorem simp1 938

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

Syntax hints:   → wi 4   ∧ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  simpl1  941  simpr1  944  simp1i  947  simp1d  950  simp11  968  simp21  971  simp31  974  syld3an3  1214  3ianorr  1240  stoic4a  1361  stoic4b  1362  rsp2e  2414  issod  4074  elirr  4284  sotri2  4742  sotri3  4743  funtpg  4970  funimaexglem  5002  feq123  5058  foco2  5339  ftpg  5368  fsnunf  5383  fcofo  5444  f1oiso2  5486  riotass  5515  ovmpt2x  5649  ovmpt2ga  5650  caovimo  5714  ofeq  5734  ofrval  5742  frecsuclem3  6013  diffifi  6378  unsnfidcex  6385  unsnfidcel  6386  mulcanenq  6575  ltanqg  6590  addnnnq0  6639  distrlem4prl  6774  distrlem4pru  6775  distrprg  6778  aptipr  6831  addsrpr  6922  mulsrpr  6923  mulasssrg  6935  axmulass  7039  axpre-ltadd  7052  mul31  7239  addsubass  7318  subcan2  7333  subsub2  7336  subsub4  7341  npncan3  7346  pnpcan  7347  pnncan  7349  subcan  7363  subdi  7489  ltadd1  7533  leadd1  7534  leadd2  7535  ltsubadd  7536  lesubadd  7538  ltaddsub  7540  leaddsub  7542  lesub1  7560  lesub2  7561  ltsub1  7562  ltsub2  7563  ltaddsublt  7671  gt0add  7673  apreap  7687  lemul1  7693  reapmul1lem  7694  reapmul1  7695  reapadd1  7696  remulext1  7699  remulext2  7700  apadd2  7709  mulext2  7713  mulap0r  7715  leltap  7724  ltap  7731  recexaplem2  7742  mulcanap  7755  mulcanap2  7756  divvalap  7762  divcanap2  7768  diveqap0  7770  divrecap  7776  divrecap2  7777  divdirap  7785  divcanap3  7786  div11ap  7788  muldivdirap  7795  divcanap5  7802  redivclap  7819  div2negap  7823  apmul1  7876  ltdiv1  7946  ltmuldiv  7952  lemuldiv  7959  lt2msq1  7963  ltdiv23  7970  lediv23  7971  squeeze0  7982  gtndiv  8442  eluz2  8625  eluzsub  8648  peano2uz  8671  nn01to3  8702  divge1  8800  ledivge1le  8803  addlelt  8839  ixxssixx  8925  lbico1  8953  lbicc2  9006  icoshftf1o  9013  fzen  9062  fzrev3  9104  fzrevral2  9123  elfzo0  9191  elfzo0z  9193  fzosplitprm1  9243  qbtwnre  9265  flqwordi  9290  flqword2  9291  adddivflid  9294  flltdivnn0lt  9306  modqcl  9328  mulqmod0  9332  modqmulnn  9344  modqabs2  9360  addmodid  9374  modifeq2int  9388  modqeqmodmin  9396  iseqeq2  9435  iseqeq3  9436  expnegap0  9484  expgt1  9514  exprecap  9517  leexp2a  9529  expubnd  9533  sqdivap  9540  expnbnd  9596  bccmpl  9681  shftfibg  9708  mulreap  9751  abssubne0  9977  maxleast  10099  lemininf  10115  ltmininf  10116  climuni  10132  dvdscmulr  10224  dvdsmulcr  10225  summodnegmod  10226  modmulconst  10227  dvdsmultr2  10235  dvdsexp  10261  mulmoddvds  10263  modremain  10329  divgcdz  10363  gcdaddm  10375  dvdsgcdb  10402  gcdass  10404  mulgcd  10405  gcddiv  10408  rplpwr  10416  lcmdvdsb  10466  lcmass  10467  mulgcddvds  10476  qredeq  10478  qredeu  10479  rpmul  10480  divgcdcoprmex  10484  cncongr1  10485  rpexp  10532  rpexp12i  10534