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  2595  ifnetruedc  3670  issod  4445  elirr  4668  sotri2  5165  sotri3  5166  funtpg  5412  funimaexglem  5444  feq123  5505  ftpg  5873  fsnunf  5889  foco2  5932  fcofo  5963  f1oiso2  6006  riotass  6041  ovmpox  6190  ovmpoga  6191  caovimo  6256  ofeq  6278  ofrval  6286  fvn0elsuppb  6465  tfr1onlembxssdm  6587  tfrcllembxssdm  6600  frecsuclem  6650  frecrdg  6652  domssr  7030  mapxpen  7114  diffifi  7164  unsnfidcex  7193  unsnfidcel  7194  unfidisj  7195  undifdc  7197  ssfidc  7211  iunfidisj  7226  fissfi  7229  sbthlemi9  7248  elfir  7273  djuassen  7537  dftap2  7581  mulcanenq  7716  ltanqg  7731  addnnnq0  7780  distrlem4prl  7915  distrlem4pru  7916  distrprg  7919  aptipr  7972  addsrpr  8076  mulsrpr  8077  mulasssrg  8089  ltpsrprg  8134  axmulass  8204  axpre-ltadd  8217  mul31  8420  addsubass  8499  subcan2  8514  subsub2  8517  subsub4  8522  npncan3  8527  pnpcan  8528  pnncan  8530  subcan  8544  subdi  8675  ltadd1  8720  leadd1  8721  leadd2  8722  ltsubadd  8723  lesubadd  8725  ltaddsub  8727  leaddsub  8729  lesub1  8747  lesub2  8748  ltsub1  8749  ltsub2  8750  ltaddsublt  8862  gt0add  8864  apreap  8878  lemul1  8884  reapmul1lem  8885  reapmul1  8886  reapadd1  8887  remulext1  8890  remulext2  8891  apadd2  8900  mulext2  8904  mulap0r  8906  leltap  8916  ltap  8924  apsub1  8933  recexaplem2  8943  mulcanap  8956  mulcanap2  8957  divvalap  8965  divcanap2  8971  diveqap0  8973  divrecap  8979  divrecap2  8980  divdirap  8988  divcanap3  8989  div11ap  8991  muldivdirap  8998  divcanap5  9005  redivclap  9022  div2negap  9026  apmul1  9079  apmul2  9080  div2subap  9128  ltdiv1  9159  ltmuldiv  9165  lemuldiv  9172  lt2msq1  9176  ltdiv23  9183  lediv23  9184  squeeze0  9195  ofnegsub  9253  difgtsumgt  9664  zfidc  9673  gtndiv  9691  eluz2  9877  eluzsub  9902  peano2uz  9933  nn01to3  9967  divge1  10074  ledivge1le  10077  addlelt  10119  xaddass  10221  xleadd1  10227  xltadd1  10228  ixxssixx  10254  lbico1  10282  lbicc2  10336  icoshftf1o  10343  fzen  10397  fzrev3  10443  fzrevral2  10462  nelfzo  10508  elfzo0  10542  elfzo0z  10545  fzosplitprm1  10602  qbtwnre  10640  flqwordi  10672  flqword2  10673  adddivflid  10676  flltdivnn0lt  10688  modqcl  10712  mulqmod0  10716  modqmulnn  10728  modqabs2  10744  addmodid  10758  modifeq2int  10772  modqeqmodmin  10780  seqeq2  10837  seqeq3  10838  seq1g  10849  seqp1g  10852  exp3val  10927  expnegap0  10933  expgt1  10963  exprecap  10966  leexp2a  10978  expubnd  10982  sqdivap  10989  expnbnd  11050  mulsubdivbinom2ap  11098  bccmpl  11141  fihashss  11206  leisorel  11234  ccatass  11321  ccats1val2  11353  swrdval  11365  swrdval2  11368  swrdlen2  11379  swrdfv2  11380  pfxfv  11401  pfxn0  11405  pfxnd  11406  swrdswrd  11422  pfxswrd  11423  pfxpfx  11425  ccats1pfxeqbi  11459  s3cl  11503  s3fv0g  11508  s3fv1g  11509  s3fv2g  11510  shftfibg  11530  mulreap  11574  abssubne0  11801  maxleast  11923  lemininf  11944  ltmininf  11945  xrmaxltsup  11968  xrmaxaddlem  11970  xrmaxadd  11971  xrmineqinf  11979  xrltmininf  11980  xrminltinf  11982  xrminadd  11985  climuni  12003  reccn2ap  12023  isumz  12100  fsumsplitsnun  12130  geoisum1c  12231  prod1dc  12297  efltim  12409  dvdscmulr  12531  dvdsmulcr  12532  summodnegmod  12533  modmulconst  12534  dvdsmultr2  12544  dvdsexp  12572  mulmoddvds  12574  modremain  12640  divgcdz  12692  gcdaddm  12705  dvdsgcdb  12734  gcdass  12736  mulgcd  12737  gcddiv  12740  rplpwr  12748  uzwodc  12758  lcmdvdsb  12806  lcmass  12807  mulgcddvds  12816  qredeq  12818  qredeu  12819  rpmul  12820  divgcdcoprmex  12824  cncongr1  12825  rpexp  12875  rpexp12i  12877  odzcllem  12965  odzdvds  12968  odzphi  12969  pythagtriplem15  13001  pcpremul  13016  pcdiv  13025  pcqmul  13026  pcqdiv  13030  dvdsprmpweq  13058  sumhashdc  13070  pcfaclem  13072  qexpz  13075  ballotfilemfrcn0  13217  ctinf  13265  setsvala  13327  ressressg  13372  ressabsg  13373  rngbaseg  13433  ptex  13561  issubmnd  13739  ress0g  13740  imasmnd2  13749  gsumfzz  13792  grpasscan2  13861  grpidrcan  13862  grpidlcan  13863  grpinvadd  13875  grpsubeq0  13883  grppncan  13888  dfgrp3m  13896  grpsubpropd2  13902  pwsinvg  13909  imasgrp2  13911  mhmmnd  13917  mulgnegneg  13942  mulgaddcomlem  13946  mulgaddcom  13947  mulginvcom  13948  mulgmodid  13962  issubg  13974  nsgconj  14007  nsgid  14016  quselbasg  14031  quseccl0g  14032  ghmnsgima  14069  cmn4  14106  ablinvadd  14111  ablsub4  14114  abladdsub4  14115  ablpncan2  14117  rngpropd  14183  imasrng  14184  issrg  14193  ringidss  14257  ringcom  14259  imasring  14292  unitmulcl  14343  unitmulclb  14344  dvrcl  14365  unitdvcl  14366  dvrcan1  14370  dvrcan3  14371  issubrng  14430  subrngpropd  14447  rrgeq0  14496  islmod  14551  lmodcom  14593  rmodislmodlem  14610  rmodislmod  14611  lss0cl  14629  lssvnegcl  14636  lssintclm  14644  lssincl  14645  lspss  14659  lspun  14662  lspsnvsi  14678  lsslsp  14689  rnglidlmmgm  14756  rnglidlmsgrp  14757  rnglidlrng  14758  qus2idrng  14785  qusmulrng  14792  psrbaglecl  14936  psrbagcon  14938  2basgeng  15059  clsss  15095  ntrss  15096  ntrin  15101  neiss  15127  restco  15151  restabs  15152  lmconst  15193  psmetsym  15306  psmetge0  15308  xmetge0  15342  xmetsym  15345  xmetresbl  15417  mopni3  15461  bdxmet  15478  bdmopn  15481  txmetcnp  15495  dvfvalap  15658  dvid  15672  dvidre  15674  dvcnp2cntop  15676  elplyr  15717  ply1term  15720  ptolemy  15801  rpcxpadd  15882  rpmulcxp  15886  rpdivcxp  15888  cxpmul  15889  rpcxple2  15895  rpcxplt2  15896  cxpcom  15915  rplogbval  15922  rplogbcl  15923  rprelogbmulexp  15933  relogbexpap  15935  logbleb  15938  logblt  15939  rplogbcxp  15940  rpcxplogb  15941  sgmppw  15972  lgslem1  15985  lgsfcl2  15991  lgsneg  16009  lgsne0  16023  lgssq2  16026  lgsdirnn0  16032  gausslemma2dlem1a  16043  lgsquad  16065  2lgsoddprmlem2  16091  funvtxvalg  16143  funiedgvalg  16144  lpvtx  16186  upgrex  16210  subumgredg2en  16378  iedginwlk  16464  eulerpathprum  16587  gfsumsn  16979