Theorem simp1 1024

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  simpl1  1027  simpr1  1030  simp1i  1033  simp1d  1036  simp11  1054  simp21  1057  simp31  1060  syld3an3  1319  3ianorr  1346  intn3an1d  1393  stoic4a  1477  stoic4b  1478  rsp2e  2584  ifnetruedc  3653  issod  4422  elirr  4645  sotri2  5141  sotri3  5142  funtpg  5388  funimaexglem  5420  feq123  5481  ftpg  5846  fsnunf  5862  foco2  5904  fcofo  5935  f1oiso2  5978  riotass  6011  ovmpox  6160  ovmpoga  6161  caovimo  6226  ofeq  6247  ofrval  6255  fvn0elsuppb  6430  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  frecsuclem  6615  frecrdg  6617  domssr  6994  mapxpen  7077  diffifi  7126  unsnfidcex  7155  unsnfidcel  7156  unfidisj  7157  undifdc  7159  ssfidc  7173  iunfidisj  7188  sbthlemi9  7207  elfir  7215  djuassen  7475  dftap2  7513  mulcanenq  7648  ltanqg  7663  addnnnq0  7712  distrlem4prl  7847  distrlem4pru  7848  distrprg  7851  aptipr  7904  addsrpr  8008  mulsrpr  8009  mulasssrg  8021  ltpsrprg  8066  axmulass  8136  axpre-ltadd  8149  mul31  8353  addsubass  8432  subcan2  8447  subsub2  8450  subsub4  8455  npncan3  8460  pnpcan  8461  pnncan  8463  subcan  8477  subdi  8607  ltadd1  8652  leadd1  8653  leadd2  8654  ltsubadd  8655  lesubadd  8657  ltaddsub  8659  leaddsub  8661  lesub1  8679  lesub2  8680  ltsub1  8681  ltsub2  8682  ltaddsublt  8794  gt0add  8796  apreap  8810  lemul1  8816  reapmul1lem  8817  reapmul1  8818  reapadd1  8819  remulext1  8822  remulext2  8823  apadd2  8832  mulext2  8836  mulap0r  8838  leltap  8848  ltap  8856  apsub1  8865  recexaplem2  8875  mulcanap  8888  mulcanap2  8889  divvalap  8897  divcanap2  8903  diveqap0  8905  divrecap  8911  divrecap2  8912  divdirap  8920  divcanap3  8921  div11ap  8923  muldivdirap  8930  divcanap5  8937  redivclap  8954  div2negap  8958  apmul1  9011  apmul2  9012  div2subap  9060  ltdiv1  9091  ltmuldiv  9097  lemuldiv  9104  lt2msq1  9108  ltdiv23  9115  lediv23  9116  squeeze0  9127  ofnegsub  9185  difgtsumgt  9592  gtndiv  9618  eluz2  9804  eluzsub  9829  peano2uz  9860  nn01to3  9894  divge1  10001  ledivge1le  10004  addlelt  10046  xaddass  10147  xleadd1  10153  xltadd1  10154  ixxssixx  10180  lbico1  10208  lbicc2  10262  icoshftf1o  10269  fzen  10321  fzrev3  10365  fzrevral2  10384  nelfzo  10430  elfzo0  10464  elfzo0z  10467  fzosplitprm1  10524  qbtwnre  10560  flqwordi  10592  flqword2  10593  adddivflid  10596  flltdivnn0lt  10608  modqcl  10632  mulqmod0  10636  modqmulnn  10648  modqabs2  10664  addmodid  10678  modifeq2int  10692  modqeqmodmin  10700  seqeq2  10757  seqeq3  10758  seq1g  10769  seqp1g  10772  exp3val  10847  expnegap0  10853  expgt1  10883  exprecap  10886  leexp2a  10898  expubnd  10902  sqdivap  10909  expnbnd  10969  mulsubdivbinom2ap  11017  bccmpl  11060  fihashss  11124  leisorel  11145  ccatass  11232  ccats1val2  11264  swrdval  11276  swrdval2  11279  swrdlen2  11290  swrdfv2  11291  pfxfv  11312  pfxn0  11316  pfxnd  11317  swrdswrd  11333  pfxswrd  11334  pfxpfx  11336  ccats1pfxeqbi  11370  s3cl  11414  s3fv0g  11419  s3fv1g  11420  s3fv2g  11421  shftfibg  11441  mulreap  11485  abssubne0  11712  maxleast  11834  lemininf  11855  ltmininf  11856  xrmaxltsup  11879  xrmaxaddlem  11881  xrmaxadd  11882  xrmineqinf  11890  xrltmininf  11891  xrminltinf  11893  xrminadd  11896  climuni  11914  reccn2ap  11934  isumz  12011  fsumsplitsnun  12041  geoisum1c  12142  prod1dc  12208  efltim  12320  dvdscmulr  12442  dvdsmulcr  12443  summodnegmod  12444  modmulconst  12445  dvdsmultr2  12455  dvdsexp  12483  mulmoddvds  12485  modremain  12551  divgcdz  12603  gcdaddm  12616  dvdsgcdb  12645  gcdass  12647  mulgcd  12648  gcddiv  12651  rplpwr  12659  uzwodc  12669  lcmdvdsb  12717  lcmass  12718  mulgcddvds  12727  qredeq  12729  qredeu  12730  rpmul  12731  divgcdcoprmex  12735  cncongr1  12736  rpexp  12786  rpexp12i  12788  odzcllem  12876  odzdvds  12879  odzphi  12880  pythagtriplem15  12912  pcpremul  12927  pcdiv  12936  pcqmul  12937  pcqdiv  12941  dvdsprmpweq  12969  sumhashdc  12981  pcfaclem  12983  qexpz  12986  ctinf  13112  setsvala  13174  ressressg  13219  ressabsg  13220  rngbaseg  13280  ptex  13408  issubmnd  13586  ress0g  13587  imasmnd2  13596  gsumfzz  13639  grpasscan2  13708  grpidrcan  13709  grpidlcan  13710  grpinvadd  13722  grpsubeq0  13730  grppncan  13735  dfgrp3m  13743  grpsubpropd2  13749  pwsinvg  13756  imasgrp2  13758  mhmmnd  13764  mulgnegneg  13789  mulgaddcomlem  13793  mulgaddcom  13794  mulginvcom  13795  mulgmodid  13809  issubg  13821  nsgconj  13854  nsgid  13863  quselbasg  13878  quseccl0g  13879  ghmnsgima  13916  cmn4  13953  ablinvadd  13958  ablsub4  13961  abladdsub4  13962  ablpncan2  13964  rngpropd  14030  imasrng  14031  issrg  14040  ringidss  14104  ringcom  14106  imasring  14139  unitmulcl  14189  unitmulclb  14190  dvrcl  14211  unitdvcl  14212  dvrcan1  14216  dvrcan3  14217  issubrng  14275  subrngpropd  14292  rrgeq0  14341  islmod  14367  lmodcom  14409  rmodislmodlem  14426  rmodislmod  14427  lss0cl  14445  lssvnegcl  14452  lssintclm  14460  lssincl  14461  lspss  14475  lspun  14478  lspsnvsi  14494  lsslsp  14505  rnglidlmmgm  14572  rnglidlmsgrp  14573  rnglidlrng  14574  qus2idrng  14601  qusmulrng  14608  psrbaglecl  14751  psrbagcon  14752  2basgeng  14873  clsss  14909  ntrss  14910  ntrin  14915  neiss  14941  restco  14965  restabs  14966  lmconst  15007  psmetsym  15120  psmetge0  15122  xmetge0  15156  xmetsym  15159  xmetresbl  15231  mopni3  15275  bdxmet  15292  bdmopn  15295  txmetcnp  15309  dvfvalap  15472  dvid  15486  dvidre  15488  dvcnp2cntop  15490  elplyr  15531  ply1term  15534  ptolemy  15615  rpcxpadd  15696  rpmulcxp  15700  rpdivcxp  15702  cxpmul  15703  rpcxple2  15709  rpcxplt2  15710  cxpcom  15729  rplogbval  15736  rplogbcl  15737  rprelogbmulexp  15747  relogbexpap  15749  logbleb  15752  logblt  15753  rplogbcxp  15754  rpcxplogb  15755  sgmppw  15786  lgslem1  15799  lgsfcl2  15805  lgsneg  15823  lgsne0  15837  lgssq2  15840  lgsdirnn0  15846  gausslemma2dlem1a  15857  lgsquad  15879  2lgsoddprmlem2  15905  funvtxvalg  15957  funiedgvalg  15958  lpvtx  16000  upgrex  16024  subumgredg2en  16192  iedginwlk  16278  eulerpathprum  16401  gfsumsn  16794