Theorem simp1 1000

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  simpl1  1003  simpr1  1006  simp1i  1009  simp1d  1012  simp11  1030  simp21  1033  simp31  1036  syld3an3  1295  3ianorr  1322  intn3an1d  1368  stoic4a  1452  stoic4b  1453  rsp2e  2558  ifnetruedc  3615  issod  4371  elirr  4594  sotri2  5086  sotri3  5087  funtpg  5331  funimaexglem  5363  feq123  5424  ftpg  5778  fsnunf  5794  foco2  5832  fcofo  5863  f1oiso2  5906  riotass  5937  ovmpox  6084  ovmpoga  6085  caovimo  6150  ofeq  6171  ofrval  6179  tfr1onlembxssdm  6439  tfrcllembxssdm  6452  frecsuclem  6502  frecrdg  6504  domssr  6879  mapxpen  6957  diffifi  7003  unsnfidcex  7029  unsnfidcel  7030  unfidisj  7031  undifdc  7033  ssfidc  7046  iunfidisj  7060  sbthlemi9  7079  elfir  7087  djuassen  7342  dftap2  7376  mulcanenq  7511  ltanqg  7526  addnnnq0  7575  distrlem4prl  7710  distrlem4pru  7711  distrprg  7714  aptipr  7767  addsrpr  7871  mulsrpr  7872  mulasssrg  7884  ltpsrprg  7929  axmulass  7999  axpre-ltadd  8012  mul31  8216  addsubass  8295  subcan2  8310  subsub2  8313  subsub4  8318  npncan3  8323  pnpcan  8324  pnncan  8326  subcan  8340  subdi  8470  ltadd1  8515  leadd1  8516  leadd2  8517  ltsubadd  8518  lesubadd  8520  ltaddsub  8522  leaddsub  8524  lesub1  8542  lesub2  8543  ltsub1  8544  ltsub2  8545  ltaddsublt  8657  gt0add  8659  apreap  8673  lemul1  8679  reapmul1lem  8680  reapmul1  8681  reapadd1  8682  remulext1  8685  remulext2  8686  apadd2  8695  mulext2  8699  mulap0r  8701  leltap  8711  ltap  8719  apsub1  8728  recexaplem2  8738  mulcanap  8751  mulcanap2  8752  divvalap  8760  divcanap2  8766  diveqap0  8768  divrecap  8774  divrecap2  8775  divdirap  8783  divcanap3  8784  div11ap  8786  muldivdirap  8793  divcanap5  8800  redivclap  8817  div2negap  8821  apmul1  8874  apmul2  8875  div2subap  8923  ltdiv1  8954  ltmuldiv  8960  lemuldiv  8967  lt2msq1  8971  ltdiv23  8978  lediv23  8979  squeeze0  8990  ofnegsub  9048  difgtsumgt  9455  gtndiv  9481  eluz2  9667  eluzsub  9691  peano2uz  9717  nn01to3  9751  divge1  9858  ledivge1le  9861  addlelt  9903  xaddass  10004  xleadd1  10010  xltadd1  10011  ixxssixx  10037  lbico1  10065  lbicc2  10119  icoshftf1o  10126  fzen  10178  fzrev3  10222  fzrevral2  10241  nelfzo  10287  elfzo0  10319  elfzo0z  10321  fzosplitprm1  10376  qbtwnre  10412  flqwordi  10444  flqword2  10445  adddivflid  10448  flltdivnn0lt  10460  modqcl  10484  mulqmod0  10488  modqmulnn  10500  modqabs2  10516  addmodid  10530  modifeq2int  10544  modqeqmodmin  10552  seqeq2  10609  seqeq3  10610  seq1g  10621  seqp1g  10624  exp3val  10699  expnegap0  10705  expgt1  10735  exprecap  10738  leexp2a  10750  expubnd  10754  sqdivap  10761  expnbnd  10821  mulsubdivbinom2ap  10869  bccmpl  10912  fihashss  10974  leisorel  10995  ccatass  11078  ccats1val2  11106  swrdval  11115  swrdval2  11118  swrdlen2  11129  swrdfv2  11130  pfxfv  11149  pfxn0  11153  pfxnd  11154  swrdswrd  11170  pfxswrd  11171  pfxpfx  11173  shftfibg  11181  mulreap  11225  abssubne0  11452  maxleast  11574  lemininf  11595  ltmininf  11596  xrmaxltsup  11619  xrmaxaddlem  11621  xrmaxadd  11622  xrmineqinf  11630  xrltmininf  11631  xrminltinf  11633  xrminadd  11636  climuni  11654  reccn2ap  11674  isumz  11750  fsumsplitsnun  11780  geoisum1c  11881  prod1dc  11947  efltim  12059  dvdscmulr  12181  dvdsmulcr  12182  summodnegmod  12183  modmulconst  12184  dvdsmultr2  12194  dvdsexp  12222  mulmoddvds  12224  modremain  12290  divgcdz  12342  gcdaddm  12355  dvdsgcdb  12384  gcdass  12386  mulgcd  12387  gcddiv  12390  rplpwr  12398  uzwodc  12408  lcmdvdsb  12456  lcmass  12457  mulgcddvds  12466  qredeq  12468  qredeu  12469  rpmul  12470  divgcdcoprmex  12474  cncongr1  12475  rpexp  12525  rpexp12i  12527  odzcllem  12615  odzdvds  12618  odzphi  12619  pythagtriplem15  12651  pcpremul  12666  pcdiv  12675  pcqmul  12676  pcqdiv  12680  dvdsprmpweq  12708  sumhashdc  12720  pcfaclem  12722  qexpz  12725  ctinf  12851  setsvala  12913  ressressg  12957  ressabsg  12958  rngbaseg  13018  ptex  13146  issubmnd  13324  ress0g  13325  imasmnd2  13334  gsumfzz  13377  grpasscan2  13446  grpidrcan  13447  grpidlcan  13448  grpinvadd  13460  grpsubeq0  13468  grppncan  13473  dfgrp3m  13481  grpsubpropd2  13487  pwsinvg  13494  imasgrp2  13496  mhmmnd  13502  mulgnegneg  13527  mulgaddcomlem  13531  mulgaddcom  13532  mulginvcom  13533  mulgmodid  13547  issubg  13559  nsgconj  13592  nsgid  13601  quselbasg  13616  quseccl0g  13617  ghmnsgima  13654  cmn4  13691  ablinvadd  13696  ablsub4  13699  abladdsub4  13700  ablpncan2  13702  rngpropd  13767  imasrng  13768  issrg  13777  ringidss  13841  ringcom  13843  imasring  13876  unitmulcl  13925  unitmulclb  13926  dvrcl  13947  unitdvcl  13948  dvrcan1  13952  dvrcan3  13953  issubrng  14011  subrngpropd  14028  rrgeq0  14077  islmod  14103  lmodcom  14145  rmodislmodlem  14162  rmodislmod  14163  lss0cl  14181  lssvnegcl  14188  lssintclm  14196  lssincl  14197  lspss  14211  lspun  14214  lspsnvsi  14230  lsslsp  14241  rnglidlmmgm  14308  rnglidlmsgrp  14309  rnglidlrng  14310  qus2idrng  14337  qusmulrng  14344  2basgeng  14604  clsss  14640  ntrss  14641  ntrin  14646  neiss  14672  restco  14696  restabs  14697  lmconst  14738  psmetsym  14851  psmetge0  14853  xmetge0  14887  xmetsym  14890  xmetresbl  14962  mopni3  15006  bdxmet  15023  bdmopn  15026  txmetcnp  15040  dvfvalap  15203  dvid  15217  dvidre  15219  dvcnp2cntop  15221  elplyr  15262  ply1term  15265  ptolemy  15346  rpcxpadd  15427  rpmulcxp  15431  rpdivcxp  15433  cxpmul  15434  rpcxple2  15440  rpcxplt2  15441  cxpcom  15460  rplogbval  15467  rplogbcl  15468  rprelogbmulexp  15478  relogbexpap  15480  logbleb  15483  logblt  15484  rplogbcxp  15485  rpcxplogb  15486  sgmppw  15514  lgslem1  15527  lgsfcl2  15533  lgsneg  15551  lgsne0  15565  lgssq2  15568  lgsdirnn0  15574  gausslemma2dlem1a  15585  lgsquad  15607  2lgsoddprmlem2  15633  funvtxvalg  15685  funiedgvalg  15686  lpvtx  15725  upgrex  15749