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  4464  elirr  4688  sotri2  5185  sotri3  5186  funtpg  5432  funimaexglem  5464  feq123  5525  ftpg  5899  fsnunf  5915  foco2  5959  fcofo  5990  f1oiso2  6033  riotass  6068  ovmpox  6217  ovmpoga  6218  caovimo  6283  ofeq  6305  ofrval  6313  fvn0elsuppb  6492  tfr1onlembxssdm  6614  tfrcllembxssdm  6627  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  diffifi  7198  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  ssfidc  7245  iunfidisj  7260  fissfi  7263  sbthlemi9  7282  elfir  7307  fdcf1  7316  djuassen  7574  dftap2  7618  mulcanenq  7753  ltanqg  7768  addnnnq0  7817  distrlem4prl  7952  distrlem4pru  7953  distrprg  7956  aptipr  8009  addsrpr  8113  mulsrpr  8114  mulasssrg  8126  ltpsrprg  8171  axmulass  8241  axpre-ltadd  8254  mul31  8459  addsubass  8538  subcan2  8553  subsub2  8556  subsub4  8561  npncan3  8566  pnpcan  8567  pnncan  8569  subcan  8583  subdi  8714  ltadd1  8759  leadd1  8760  leadd2  8761  ltsubadd  8762  lesubadd  8764  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  ltaddsublt  8902  gt0add  8904  apreap  8918  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  remulext1  8930  remulext2  8931  apadd2  8940  mulext2  8944  mulap0r  8946  leltap  8956  ltap  8964  apsub1  8973  recexaplem2  8983  mulcanap  8996  mulcanap2  8997  divvalap  9007  divcanap2  9013  diveqap0  9015  divrecap  9021  divrecap2  9022  divdirap  9030  divcanap3  9031  div11ap  9033  muldivdirap  9040  divcanap5  9047  redivclap  9064  div2negap  9068  apmul1  9121  apmul2  9122  div2subap  9170  ltdiv1  9201  ltmuldiv  9207  lemuldiv  9214  lt2msq1  9218  ltdiv23  9225  lediv23  9226  squeeze0  9237  ofnegsub  9295  difgtsumgt  9719  zfidc  9728  gtndiv  9746  eluz2  9937  eluzsub  9962  peano2uz  9993  nn01to3  10027  divge1  10135  ledivge1le  10138  addlelt  10180  xaddass  10282  xleadd1  10288  xltadd1  10289  ixxssixx  10315  lbico1  10343  lbicc2  10397  icoshftf1o  10404  fzen  10458  fzrev3  10505  fzrevral2  10524  nelfzo  10570  elfzo0  10604  elfzo0z  10607  fzosplitprm1  10664  qbtwnre  10702  flqwordi  10737  flqword2  10738  adddivflid  10741  flltdivnn0lt  10753  modqcl  10777  mulqmod0  10781  modqmulnn  10793  modqabs2  10809  addmodid  10823  modifeq2int  10837  modqeqmodmin  10845  seqeq2  10902  seqeq3  10903  seq1g  10914  seqp1g  10917  exp3val  10992  expnegap0  10998  expgt1  11028  exprecap  11031  leexp2a  11043  expubnd  11047  sqdivap  11054  expnbnd  11115  mulsubdivbinom2ap  11164  bccmpl  11207  fihashss  11272  leisorel  11304  ccatass  11391  ccats1val2  11423  swrdval  11435  swrdval2  11438  swrdlen2  11449  swrdfv2  11450  pfxfv  11471  pfxn0  11475  pfxnd  11476  swrdswrd  11492  pfxswrd  11493  pfxpfx  11495  ccats1pfxeqbi  11529  s3cl  11573  s3fv0g  11578  s3fv1g  11579  s3fv2g  11580  shftfibg  11600  mulreap  11644  abssubne0  11873  maxleast  11995  lemininf  12017  ltmininf  12018  xrmaxltsup  12042  xrmaxaddlem  12044  xrmaxadd  12045  xrmineqinf  12053  xrltmininf  12054  xrminltinf  12056  xrminadd  12059  climuni  12077  reccn2ap  12097  isumz  12174  fsumsplitsnun  12204  geoisum1c  12305  prod1dc  12371  efltim  12483  dvdscmulr  12605  dvdsmulcr  12606  summodnegmod  12607  modmulconst  12608  dvdsmultr2  12618  dvdsexp  12646  mulmoddvds  12648  modremain  12714  divgcdz  12766  gcdaddm  12779  dvdsgcdb  12808  gcdass  12810  mulgcd  12811  gcddiv  12814  rplpwr  12822  uzwodc  12832  lcmdvdsb  12880  lcmass  12881  mulgcddvds  12890  qredeq  12892  qredeu  12893  rpmul  12894  divgcdcoprmex  12898  cncongr1  12899  rpexp  12950  rpexp12i  12952  odzcllem  13043  odzdvds  13046  odzphi  13047  pythagtriplem15  13079  pcpremul  13094  pcdiv  13103  pcqmul  13104  pcqdiv  13108  dvdsprmpweq  13136  sumhashdc  13148  pcfaclem  13150  qexpz  13153  ballotfilemfrcn0  13324  ctinf  13372  setsvala  13434  ressressg  13480  ressabsg  13481  rngbaseg  13541  ptex  13669  issubmnd  13806  ress0g  13807  imasmnd2  13810  grpasscan2  13920  grpidrcan  13921  grpidlcan  13922  grpinvadd  13934  grpsubeq0  13942  grppncan  13947  dfgrp3m  13955  grpsubpropd2  13961  imasgrp2  13964  mhmmnd  13970  mulgnegneg  13995  mulgaddcomlem  13999  mulgaddcom  14000  mulginvcom  14001  mulgmodid  14015  issubg  14027  nsgconj  14060  nsgid  14069  quselbasg  14084  quseccl0g  14085  ghmnsgima  14122  cmn4  14159  ablinvadd  14165  ablsub4  14168  abladdsub4  14169  ablpncan2  14171  gsumsncmn  14207  gsumconstcmn  14217  pwsinvg  14266  rngpropd  14305  imasrng  14306  issrg  14320  ringidss  14385  ringcom  14387  imasring  14420  unitmulcl  14471  unitmulclb  14472  dvrcl  14493  unitdvcl  14494  dvrcan1  14498  dvrcan3  14499  issubrng  14558  subrngpropd  14575  rrgeq0  14624  islmod  14678  lmodcom  14721  rmodislmodlem  14738  rmodislmod  14739  lss0cl  14757  lssvnegcl  14764  lssintclm  14772  lssincl  14773  lspss  14787  lspun  14790  lspsnvsi  14806  lsslsp  14817  rnglidlmmgm  14884  rnglidlmsgrp  14885  rnglidlrng  14886  qus2idrng  14913  qusmulrng  14920  assa2ass  15060  assa2ass2  15061  aspid  15068  aspss  15070  asclmul1  15080  asclmul2  15081  asclinvg  15083  psrbaglecl  15111  psrbagcon  15113  2basgeng  15235  clsss  15271  ntrss  15272  ntrin  15277  neiss  15303  restco  15327  restabs  15328  lmconst  15369  psmetsym  15482  psmetge0  15484  xmetge0  15518  xmetsym  15521  xmetresbl  15593  mopni3  15637  bdxmet  15654  bdmopn  15657  txmetcnp  15671  dvfvalap  15834  dvid  15848  dvidre  15850  dvcnp2cntop  15852  elplyr  15893  ply1term  15896  ptolemy  15978  logfac  16051  rpcxpadd  16063  rpmulcxp  16067  rpdivcxp  16069  cxpmul  16070  rpcxple2  16076  rpcxplt2  16077  cxpcom  16096  rplogbval  16103  rplogbcl  16104  rprelogbmulexp  16114  relogbexpap  16116  logbleb  16119  logblt  16120  rplogbcxp  16121  rpcxplogb  16122  sgmppw  16208  prmefexple  16230  lgslem1  16241  lgsfcl2  16247  lgsneg  16265  lgsne0  16279  lgssq2  16282  lgsdirnn0  16288  gausslemma2dlem1a  16299  lgsquad  16321  2lgsoddprmlem2  16347  funvtxvalg  16399  funiedgvalg  16400  lpvtx  16442  upgrex  16466  subumgredg2en  16634  iedginwlk  16720  eulerpathprum  16843  dichmul0or  16882