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  1430  stoic4b  1431  rsp2e  2526  issod  4313  elirr  4534  sotri2  5018  sotri3  5019  funtpg  5259  funimaexglem  5291  feq123  5349  ftpg  5692  fsnunf  5708  foco2  5745  fcofo  5775  f1oiso2  5818  riotass  5848  ovmpox  5993  ovmpoga  5994  caovimo  6058  ofeq  6075  ofrval  6083  tfr1onlembxssdm  6334  tfrcllembxssdm  6347  frecsuclem  6397  frecrdg  6399  mapxpen  6838  diffifi  6884  unsnfidcex  6909  unsnfidcel  6910  unfidisj  6911  undifdc  6913  ssfidc  6924  iunfidisj  6935  sbthlemi9  6954  elfir  6962  djuassen  7206  mulcanenq  7359  ltanqg  7374  addnnnq0  7423  distrlem4prl  7558  distrlem4pru  7559  distrprg  7562  aptipr  7615  addsrpr  7719  mulsrpr  7720  mulasssrg  7732  ltpsrprg  7777  axmulass  7847  axpre-ltadd  7860  mul31  8062  addsubass  8141  subcan2  8156  subsub2  8159  subsub4  8164  npncan3  8169  pnpcan  8170  pnncan  8172  subcan  8186  subdi  8316  ltadd1  8360  leadd1  8361  leadd2  8362  ltsubadd  8363  lesubadd  8365  ltaddsub  8367  leaddsub  8369  lesub1  8387  lesub2  8388  ltsub1  8389  ltsub2  8390  ltaddsublt  8502  gt0add  8504  apreap  8518  lemul1  8524  reapmul1lem  8525  reapmul1  8526  reapadd1  8527  remulext1  8530  remulext2  8531  apadd2  8540  mulext2  8544  mulap0r  8546  leltap  8556  ltap  8564  apsub1  8573  recexaplem2  8582  mulcanap  8595  mulcanap2  8596  divvalap  8604  divcanap2  8610  diveqap0  8612  divrecap  8618  divrecap2  8619  divdirap  8627  divcanap3  8628  div11ap  8630  muldivdirap  8637  divcanap5  8644  redivclap  8661  div2negap  8665  apmul1  8718  apmul2  8719  div2subap  8767  ltdiv1  8798  ltmuldiv  8804  lemuldiv  8811  lt2msq1  8815  ltdiv23  8822  lediv23  8823  squeeze0  8834  difgtsumgt  9295  gtndiv  9321  eluz2  9507  eluzsub  9530  peano2uz  9556  nn01to3  9590  divge1  9694  ledivge1le  9697  addlelt  9739  xaddass  9840  xleadd1  9846  xltadd1  9847  ixxssixx  9873  lbico1  9901  lbicc2  9955  icoshftf1o  9962  fzen  10013  fzrev3  10057  fzrevral2  10076  elfzo0  10152  elfzo0z  10154  fzosplitprm1  10204  qbtwnre  10227  flqwordi  10258  flqword2  10259  adddivflid  10262  flltdivnn0lt  10274  modqcl  10296  mulqmod0  10300  modqmulnn  10312  modqabs2  10328  addmodid  10342  modifeq2int  10356  modqeqmodmin  10364  seqeq2  10419  seqeq3  10420  exp3val  10492  expnegap0  10498  expgt1  10528  exprecap  10531  leexp2a  10543  expubnd  10547  sqdivap  10554  expnbnd  10613  bccmpl  10702  fihashss  10764  leisorel  10785  shftfibg  10797  mulreap  10841  abssubne0  11068  maxleast  11190  lemininf  11210  ltmininf  11211  xrmaxltsup  11234  xrmaxaddlem  11236  xrmaxadd  11237  xrmineqinf  11245  xrltmininf  11246  xrminltinf  11248  xrminadd  11251  climuni  11269  reccn2ap  11289  isumz  11365  fsumsplitsnun  11395  geoisum1c  11496  prod1dc  11562  efltim  11674  dvdscmulr  11795  dvdsmulcr  11796  summodnegmod  11797  modmulconst  11798  dvdsmultr2  11808  dvdsexp  11834  mulmoddvds  11836  modremain  11901  divgcdz  11939  gcdaddm  11952  dvdsgcdb  11981  gcdass  11983  mulgcd  11984  gcddiv  11987  rplpwr  11995  uzwodc  12005  lcmdvdsb  12051  lcmass  12052  mulgcddvds  12061  qredeq  12063  qredeu  12064  rpmul  12065  divgcdcoprmex  12069  cncongr1  12070  rpexp  12120  rpexp12i  12122  odzcllem  12209  odzdvds  12212  odzphi  12213  pythagtriplem15  12245  pcpremul  12260  pcdiv  12269  pcqmul  12270  pcqdiv  12274  dvdsprmpweq  12301  sumhashdc  12312  pcfaclem  12314  qexpz  12317  ctinf  12398  setsvala  12460  ressressg  12500  ressabsg  12501  rngbaseg  12556  grpasscan2  12804  grpidrcan  12805  grpidlcan  12806  grpinvadd  12818  grpsubeq0  12826  grppncan  12831  dfgrp3m  12839  grpsubpropd2  12845  mhmmnd  12850  mulgnegneg  12872  mulgaddcomlem  12875  mulgaddcom  12876  mulginvcom  12877  mulgmodid  12891  cmn4  12916  ablinvadd  12921  ablsub4  12924  abladdsub4  12925  ablpncan2  12927  issrg  12954  ringcom  13019  2basgeng  13162  clsss  13198  ntrss  13199  ntrin  13204  neiss  13230  restco  13254  restabs  13255  lmconst  13296  psmetsym  13409  psmetge0  13411  xmetge0  13445  xmetsym  13448  xmetresbl  13520  mopni3  13564  bdxmet  13581  bdmopn  13584  txmetcnp  13598  dvfvalap  13730  dvid  13742  dvcnp2cntop  13743  ptolemy  13825  rpcxpadd  13906  rpmulcxp  13910  rpdivcxp  13912  cxpmul  13913  rpcxple2  13918  rpcxplt2  13919  cxpcom  13937  rplogbval  13943  rplogbcl  13944  rprelogbmulexp  13954  relogbexpap  13956  logbleb  13959  logblt  13960  rplogbcxp  13961  rpcxplogb  13962  lgslem1  13981  lgsfcl2  13987  lgsneg  14005  lgsne0  14019  lgssq2  14022  lgsdirnn0  14028