Theorem simp1 987

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

Syntax hints:   → wi 4   ∧ w3a 968

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 970

This theorem is referenced by:  simpl1  990  simpr1  993  simp1i  996  simp1d  999  simp11  1017  simp21  1020  simp31  1023  syld3an3  1273  3ianorr  1299  stoic4a  1420  stoic4b  1421  rsp2e  2517  issod  4297  elirr  4518  sotri2  5001  sotri3  5002  funtpg  5239  funimaexglem  5271  feq123  5329  ftpg  5669  fsnunf  5685  foco2  5722  fcofo  5752  f1oiso2  5795  riotass  5825  ovmpox  5970  ovmpoga  5971  caovimo  6035  ofeq  6052  ofrval  6060  tfr1onlembxssdm  6311  tfrcllembxssdm  6324  frecsuclem  6374  frecrdg  6376  mapxpen  6814  diffifi  6860  unsnfidcex  6885  unsnfidcel  6886  unfidisj  6887  undifdc  6889  ssfidc  6900  iunfidisj  6911  sbthlemi9  6930  elfir  6938  djuassen  7173  mulcanenq  7326  ltanqg  7341  addnnnq0  7390  distrlem4prl  7525  distrlem4pru  7526  distrprg  7529  aptipr  7582  addsrpr  7686  mulsrpr  7687  mulasssrg  7699  ltpsrprg  7744  axmulass  7814  axpre-ltadd  7827  mul31  8029  addsubass  8108  subcan2  8123  subsub2  8126  subsub4  8131  npncan3  8136  pnpcan  8137  pnncan  8139  subcan  8153  subdi  8283  ltadd1  8327  leadd1  8328  leadd2  8329  ltsubadd  8330  lesubadd  8332  ltaddsub  8334  leaddsub  8336  lesub1  8354  lesub2  8355  ltsub1  8356  ltsub2  8357  ltaddsublt  8469  gt0add  8471  apreap  8485  lemul1  8491  reapmul1lem  8492  reapmul1  8493  reapadd1  8494  remulext1  8497  remulext2  8498  apadd2  8507  mulext2  8511  mulap0r  8513  leltap  8523  ltap  8531  apsub1  8540  recexaplem2  8549  mulcanap  8562  mulcanap2  8563  divvalap  8570  divcanap2  8576  diveqap0  8578  divrecap  8584  divrecap2  8585  divdirap  8593  divcanap3  8594  div11ap  8596  muldivdirap  8603  divcanap5  8610  redivclap  8627  div2negap  8631  apmul1  8684  apmul2  8685  div2subap  8733  ltdiv1  8763  ltmuldiv  8769  lemuldiv  8776  lt2msq1  8780  ltdiv23  8787  lediv23  8788  squeeze0  8799  difgtsumgt  9260  gtndiv  9286  eluz2  9472  eluzsub  9495  peano2uz  9521  nn01to3  9555  divge1  9659  ledivge1le  9662  addlelt  9704  xaddass  9805  xleadd1  9811  xltadd1  9812  ixxssixx  9838  lbico1  9866  lbicc2  9920  icoshftf1o  9927  fzen  9978  fzrev3  10022  fzrevral2  10041  elfzo0  10117  elfzo0z  10119  fzosplitprm1  10169  qbtwnre  10192  flqwordi  10223  flqword2  10224  adddivflid  10227  flltdivnn0lt  10239  modqcl  10261  mulqmod0  10265  modqmulnn  10277  modqabs2  10293  addmodid  10307  modifeq2int  10321  modqeqmodmin  10329  seqeq2  10384  seqeq3  10385  exp3val  10457  expnegap0  10463  expgt1  10493  exprecap  10496  leexp2a  10508  expubnd  10512  sqdivap  10519  expnbnd  10578  bccmpl  10667  fihashss  10729  leisorel  10750  shftfibg  10762  mulreap  10806  abssubne0  11033  maxleast  11155  lemininf  11175  ltmininf  11176  xrmaxltsup  11199  xrmaxaddlem  11201  xrmaxadd  11202  xrmineqinf  11210  xrltmininf  11211  xrminltinf  11213  xrminadd  11216  climuni  11234  reccn2ap  11254  isumz  11330  fsumsplitsnun  11360  geoisum1c  11461  prod1dc  11527  efltim  11639  dvdscmulr  11760  dvdsmulcr  11761  summodnegmod  11762  modmulconst  11763  dvdsmultr2  11773  dvdsexp  11799  mulmoddvds  11801  modremain  11866  divgcdz  11904  gcdaddm  11917  dvdsgcdb  11946  gcdass  11948  mulgcd  11949  gcddiv  11952  rplpwr  11960  uzwodc  11970  lcmdvdsb  12016  lcmass  12017  mulgcddvds  12026  qredeq  12028  qredeu  12029  rpmul  12030  divgcdcoprmex  12034  cncongr1  12035  rpexp  12085  rpexp12i  12087  odzcllem  12174  odzdvds  12177  odzphi  12178  pythagtriplem15  12210  pcpremul  12225  pcdiv  12234  pcqmul  12235  pcqdiv  12239  dvdsprmpweq  12266  sumhashdc  12277  pcfaclem  12279  qexpz  12282  ctinf  12363  setsvala  12425  ressid2  12454  ressval2  12455  rngbaseg  12511  2basgeng  12732  clsss  12768  ntrss  12769  ntrin  12774  neiss  12800  restco  12824  restabs  12825  lmconst  12866  psmetsym  12979  psmetge0  12981  xmetge0  13015  xmetsym  13018  xmetresbl  13090  mopni3  13134  bdxmet  13151  bdmopn  13154  txmetcnp  13168  dvfvalap  13300  dvid  13312  dvcnp2cntop  13313  ptolemy  13395  rpcxpadd  13476  rpmulcxp  13480  rpdivcxp  13482  cxpmul  13483  rpcxple2  13488  rpcxplt2  13489  cxpcom  13507  rplogbval  13513  rplogbcl  13514  rprelogbmulexp  13524  relogbexpap  13526  logbleb  13529  logblt  13530  rplogbcxp  13531  rpcxplogb  13532  lgslem1  13551  lgsfcl2  13557  lgsneg  13575  lgsne0  13589  lgssq2  13592  lgsdirnn0  13598