Theorem simp1 1028

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  simpl1  1031  simpr1  1034  simp1i  1037  simp1d  1040  simp11  1058  simp21  1061  simp31  1064  syld3an3  1323  3ianorr  1350  intn3an1d  1397  stoic4a  1481  stoic4b  1482  rsp2e  2601  ifnetruedc  3684  issod  4466  elirr  4690  sotri2  5188  sotri3  5189  funtpg  5435  funimaexglem  5467  feq123  5528  ftpg  5902  fsnunf  5918  foco2  5962  fcofo  5993  f1oiso2  6036  riotass  6071  ovmpox  6220  ovmpoga  6221  caovimo  6286  ofeq  6308  ofrval  6317  fvn0elsuppb  6496  tfr1onlembxssdm  6619  tfrcllembxssdm  6632  frecsuclem  6682  frecrdg  6684  mapm  6975  domssr  7070  mapxpen  7154  diffifi  7204  unsnfidcex  7233  unsnfidcel  7234  unfidisj  7235  undifdc  7237  ssfidc  7251  iunfidisj  7266  fissfi  7269  sbthlemi9  7289  elfir  7313  fdcf1  7322  djuassen  7580  dftap2  7624  mulcanenq  7759  ltanqg  7774  addnnnq0  7823  distrlem4prl  7958  distrlem4pru  7959  distrprg  7962  aptipr  8015  addsrpr  8119  mulsrpr  8120  mulasssrg  8132  ltpsrprg  8177  axmulass  8247  axpre-ltadd  8260  mul31  8465  addsubass  8544  subcan2  8559  subsub2  8562  subsub4  8567  npncan3  8572  pnpcan  8573  pnncan  8575  subcan  8589  subdi  8720  ltadd1  8765  leadd1  8766  leadd2  8767  ltsubadd  8768  lesubadd  8770  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  ltaddsublt  8908  gt0add  8910  apreap  8924  lemul1  8930  reapmul1lem  8931  reapmul1  8932  reapadd1  8933  remulext1  8936  remulext2  8937  apadd2  8946  mulext2  8950  mulap0r  8952  leltap  8962  ltap  8970  apsub1  8979  recexaplem2  8989  mulcanap  9002  mulcanap2  9003  divvalap  9013  divcanap2  9019  diveqap0  9021  divrecap  9027  divrecap2  9028  divdirap  9036  divcanap3  9037  div11ap  9039  muldivdirap  9046  divcanap5  9053  redivclap  9070  div2negap  9074  apmul1  9127  apmul2  9128  div2subap  9176  ltdiv1  9207  ltmuldiv  9213  lemuldiv  9220  lt2msq1  9224  ltdiv23  9231  lediv23  9232  squeeze0  9243  ofsubeq0  9301  ofnegsub  9302  difgtsumgt  9724  zfidc  9733  gtndiv  9752  eluz2  9943  eluzsub  9968  peano2uz  9999  nn01to3  10033  divge1  10141  ledivge1le  10144  addlelt  10186  xaddass  10288  xleadd1  10294  xltadd1  10295  ixxssixx  10321  lbico1  10349  lbicc2  10403  icoshftf1o  10410  fzen  10464  fzrev3  10511  fzrevral2  10530  nelfzo  10576  elfzo0  10610  elfzo0z  10613  fzosplitprm1  10670  qbtwnre  10708  flqwordi  10744  flqword2  10745  adddivflid  10748  flltdivnn0lt  10760  modqcl  10784  mulqmod0  10788  modqmulnn  10800  modqabs2  10816  addmodid  10830  modifeq2int  10844  modqeqmodmin  10852  seqeq2  10909  seqeq3  10910  seq1g  10921  seqp1g  10924  exp3val  10999  expnegap0  11005  expgt1  11035  exprecap  11038  leexp2a  11050  expubnd  11054  sqdivap  11061  expnbnd  11122  mulsubdivbinom2ap  11171  bccmpl  11214  fihashss  11279  leisorel  11311  ccatass  11398  ccats1val2  11430  swrdval  11442  swrdval2  11445  swrdlen2  11456  swrdfv2  11457  pfxfv  11478  pfxn0  11482  pfxnd  11483  swrdswrd  11499  pfxswrd  11500  pfxpfx  11502  ccats1pfxeqbi  11536  s3cl  11580  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftfibg  11607  mulreap  11651  abssubne0  11880  maxleast  12002  lemininf  12024  ltmininf  12025  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrmineqinf  12060  xrltmininf  12061  xrminltinf  12063  xrminadd  12066  climuni  12084  reccn2ap  12104  isumz  12181  fsumsplitsnun  12211  geoisum1c  12312  prod1dc  12378  efltim  12490  dvdscmulr  12612  dvdsmulcr  12613  summodnegmod  12614  modmulconst  12615  dvdsmultr2  12625  dvdsexp  12653  mulmoddvds  12655  modremain  12721  divgcdz  12773  gcdaddm  12786  dvdsgcdb  12815  gcdass  12817  mulgcd  12818  gcddiv  12821  rplpwr  12829  uzwodc  12839  lcmdvdsb  12887  lcmass  12888  mulgcddvds  12897  qredeq  12899  qredeu  12900  rpmul  12901  divgcdcoprmex  12905  cncongr1  12906  rpexp  12957  rpexp12i  12959  odzcllem  13050  odzdvds  13053  odzphi  13054  pythagtriplem15  13086  pcpremul  13101  pcdiv  13110  pcqmul  13111  pcqdiv  13115  dvdsprmpweq  13143  sumhashdc  13155  pcfaclem  13157  qexpz  13160  ballotfilemfrcn0  13331  ctinf  13379  setsvala  13441  ressressg  13488  ressabsg  13489  rngbaseg  13549  ptex  13677  issubmnd  13814  ress0g  13815  imasmnd2  13818  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grpsubeq0  13950  grppncan  13955  dfgrp3m  13963  grpsubpropd2  13969  imasgrp2  13972  mhmmnd  13978  mulgnegneg  14003  mulgaddcomlem  14007  mulgaddcom  14008  mulginvcom  14009  mulgmodid  14023  issubg  14035  nsgconj  14068  nsgid  14077  quselbasg  14092  quseccl0g  14093  ghmnsgima  14130  cmn4  14198  ablinvadd  14204  ablsub4  14207  abladdsub4  14208  ablpncan2  14210  gsumsncmn  14246  gsumconstcmn  14266  pwsinvg  14322  rngpropd  14361  imasrng  14362  issrg  14376  ringidss  14441  ringcom  14443  imasring  14478  unitmulcl  14529  unitmulclb  14530  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  issubrng  14616  subrngpropd  14633  rrgeq0  14682  islmod  14736  lmodcom  14779  rmodislmodlem  14796  rmodislmod  14797  lss0cl  14815  lssvnegcl  14822  lssintclm  14830  lssincl  14831  lspss  14845  lspun  14848  lspsnvsi  14864  lsslsp  14875  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  qus2idrng  14971  qusmulrng  14978  assa2ass  15118  assa2ass2  15119  aspid  15126  aspss  15128  asclmul1  15138  asclmul2  15139  asclinvg  15141  psrbagdceq  15168  snifpsrbagfi  15169  psrbaglecl  15173  psrbagcon  15174  psrbagconclfi  15182  psrbagfidceq  15184  2basgeng  15341  clsss  15377  ntrss  15378  ntrin  15383  neiss  15409  restco  15433  restabs  15434  lmconst  15475  psmetsym  15588  psmetge0  15590  xmetge0  15624  xmetsym  15627  xmetresbl  15699  mopni3  15743  bdxmet  15760  bdmopn  15763  txmetcnp  15777  dvfvalap  15940  dvid  15954  dvidre  15956  dvcnp2cntop  15958  elplyr  15999  ply1term  16002  ptolemy  16084  logfac  16159  rpcxpadd  16171  rpmulcxp  16175  rpdivcxp  16177  cxpmul  16178  rpcxple2  16186  rpcxplt2  16187  cxpcom  16206  rplogbval  16214  rplogbcl  16215  rprelogbmulexp  16225  relogbexpap  16227  logbleb  16230  logblt  16231  rplogbcxp  16232  rpcxplogb  16233  sgmppw  16319  prmefexple  16341  lgslem1  16357  lgsfcl2  16363  lgsneg  16381  lgsne0  16395  lgssq2  16398  lgsdirnn0  16404  gausslemma2dlem1a  16415  lgsquad  16437  2lgsoddprmlem2  16463  funvtxvalg  16515  funiedgvalg  16516  lpvtx  16558  upgrex  16582  subumgredg2en  16750  iedginwlk  16836  eulerpathprum  16959  dichmul0or  16998