Theorem simp1 1023

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  simpl1  1026  simpr1  1029  simp1i  1032  simp1d  1035  simp11  1053  simp21  1056  simp31  1059  syld3an3  1318  3ianorr  1345  intn3an1d  1392  stoic4a  1476  stoic4b  1477  rsp2e  2583  ifnetruedc  3649  issod  4416  elirr  4639  sotri2  5134  sotri3  5135  funtpg  5381  funimaexglem  5413  feq123  5474  ftpg  5838  fsnunf  5854  foco2  5894  fcofo  5925  f1oiso2  5968  riotass  6001  ovmpox  6150  ovmpoga  6151  caovimo  6216  ofeq  6238  ofrval  6246  tfr1onlembxssdm  6509  tfrcllembxssdm  6522  frecsuclem  6572  frecrdg  6574  domssr  6951  mapxpen  7034  diffifi  7083  unsnfidcex  7112  unsnfidcel  7113  unfidisj  7114  undifdc  7116  ssfidc  7130  iunfidisj  7145  sbthlemi9  7164  elfir  7172  djuassen  7432  dftap2  7470  mulcanenq  7605  ltanqg  7620  addnnnq0  7669  distrlem4prl  7804  distrlem4pru  7805  distrprg  7808  aptipr  7861  addsrpr  7965  mulsrpr  7966  mulasssrg  7978  ltpsrprg  8023  axmulass  8093  axpre-ltadd  8106  mul31  8310  addsubass  8389  subcan2  8404  subsub2  8407  subsub4  8412  npncan3  8417  pnpcan  8418  pnncan  8420  subcan  8434  subdi  8564  ltadd1  8609  leadd1  8610  leadd2  8611  ltsubadd  8612  lesubadd  8614  ltaddsub  8616  leaddsub  8618  lesub1  8636  lesub2  8637  ltsub1  8638  ltsub2  8639  ltaddsublt  8751  gt0add  8753  apreap  8767  lemul1  8773  reapmul1lem  8774  reapmul1  8775  reapadd1  8776  remulext1  8779  remulext2  8780  apadd2  8789  mulext2  8793  mulap0r  8795  leltap  8805  ltap  8813  apsub1  8822  recexaplem2  8832  mulcanap  8845  mulcanap2  8846  divvalap  8854  divcanap2  8860  diveqap0  8862  divrecap  8868  divrecap2  8869  divdirap  8877  divcanap3  8878  div11ap  8880  muldivdirap  8887  divcanap5  8894  redivclap  8911  div2negap  8915  apmul1  8968  apmul2  8969  div2subap  9017  ltdiv1  9048  ltmuldiv  9054  lemuldiv  9061  lt2msq1  9065  ltdiv23  9072  lediv23  9073  squeeze0  9084  ofnegsub  9142  difgtsumgt  9549  gtndiv  9575  eluz2  9761  eluzsub  9786  peano2uz  9817  nn01to3  9851  divge1  9958  ledivge1le  9961  addlelt  10003  xaddass  10104  xleadd1  10110  xltadd1  10111  ixxssixx  10137  lbico1  10165  lbicc2  10219  icoshftf1o  10226  fzen  10278  fzrev3  10322  fzrevral2  10341  nelfzo  10387  elfzo0  10421  elfzo0z  10424  fzosplitprm1  10481  qbtwnre  10517  flqwordi  10549  flqword2  10550  adddivflid  10553  flltdivnn0lt  10565  modqcl  10589  mulqmod0  10593  modqmulnn  10605  modqabs2  10621  addmodid  10635  modifeq2int  10649  modqeqmodmin  10657  seqeq2  10714  seqeq3  10715  seq1g  10726  seqp1g  10729  exp3val  10804  expnegap0  10810  expgt1  10840  exprecap  10843  leexp2a  10855  expubnd  10859  sqdivap  10866  expnbnd  10926  mulsubdivbinom2ap  10974  bccmpl  11017  fihashss  11081  leisorel  11102  ccatass  11189  ccats1val2  11221  swrdval  11233  swrdval2  11236  swrdlen2  11247  swrdfv2  11248  pfxfv  11269  pfxn0  11273  pfxnd  11274  swrdswrd  11290  pfxswrd  11291  pfxpfx  11293  ccats1pfxeqbi  11327  s3cl  11371  s3fv0g  11376  s3fv1g  11377  s3fv2g  11378  shftfibg  11385  mulreap  11429  abssubne0  11656  maxleast  11778  lemininf  11799  ltmininf  11800  xrmaxltsup  11823  xrmaxaddlem  11825  xrmaxadd  11826  xrmineqinf  11834  xrltmininf  11835  xrminltinf  11837  xrminadd  11840  climuni  11858  reccn2ap  11878  isumz  11955  fsumsplitsnun  11985  geoisum1c  12086  prod1dc  12152  efltim  12264  dvdscmulr  12386  dvdsmulcr  12387  summodnegmod  12388  modmulconst  12389  dvdsmultr2  12399  dvdsexp  12427  mulmoddvds  12429  modremain  12495  divgcdz  12547  gcdaddm  12560  dvdsgcdb  12589  gcdass  12591  mulgcd  12592  gcddiv  12595  rplpwr  12603  uzwodc  12613  lcmdvdsb  12661  lcmass  12662  mulgcddvds  12671  qredeq  12673  qredeu  12674  rpmul  12675  divgcdcoprmex  12679  cncongr1  12680  rpexp  12730  rpexp12i  12732  odzcllem  12820  odzdvds  12823  odzphi  12824  pythagtriplem15  12856  pcpremul  12871  pcdiv  12880  pcqmul  12881  pcqdiv  12885  dvdsprmpweq  12913  sumhashdc  12925  pcfaclem  12927  qexpz  12930  ctinf  13056  setsvala  13118  ressressg  13163  ressabsg  13164  rngbaseg  13224  ptex  13352  issubmnd  13530  ress0g  13531  imasmnd2  13540  gsumfzz  13583  grpasscan2  13652  grpidrcan  13653  grpidlcan  13654  grpinvadd  13666  grpsubeq0  13674  grppncan  13679  dfgrp3m  13687  grpsubpropd2  13693  pwsinvg  13700  imasgrp2  13702  mhmmnd  13708  mulgnegneg  13733  mulgaddcomlem  13737  mulgaddcom  13738  mulginvcom  13739  mulgmodid  13753  issubg  13765  nsgconj  13798  nsgid  13807  quselbasg  13822  quseccl0g  13823  ghmnsgima  13860  cmn4  13897  ablinvadd  13902  ablsub4  13905  abladdsub4  13906  ablpncan2  13908  rngpropd  13974  imasrng  13975  issrg  13984  ringidss  14048  ringcom  14050  imasring  14083  unitmulcl  14133  unitmulclb  14134  dvrcl  14155  unitdvcl  14156  dvrcan1  14160  dvrcan3  14161  issubrng  14219  subrngpropd  14236  rrgeq0  14285  islmod  14311  lmodcom  14353  rmodislmodlem  14370  rmodislmod  14371  lss0cl  14389  lssvnegcl  14396  lssintclm  14404  lssincl  14405  lspss  14419  lspun  14422  lspsnvsi  14438  lsslsp  14449  rnglidlmmgm  14516  rnglidlmsgrp  14517  rnglidlrng  14518  qus2idrng  14545  qusmulrng  14552  2basgeng  14812  clsss  14848  ntrss  14849  ntrin  14854  neiss  14880  restco  14904  restabs  14905  lmconst  14946  psmetsym  15059  psmetge0  15061  xmetge0  15095  xmetsym  15098  xmetresbl  15170  mopni3  15214  bdxmet  15231  bdmopn  15234  txmetcnp  15248  dvfvalap  15411  dvid  15425  dvidre  15427  dvcnp2cntop  15429  elplyr  15470  ply1term  15473  ptolemy  15554  rpcxpadd  15635  rpmulcxp  15639  rpdivcxp  15641  cxpmul  15642  rpcxple2  15648  rpcxplt2  15649  cxpcom  15668  rplogbval  15675  rplogbcl  15676  rprelogbmulexp  15686  relogbexpap  15688  logbleb  15691  logblt  15692  rplogbcxp  15693  rpcxplogb  15694  sgmppw  15722  lgslem1  15735  lgsfcl2  15741  lgsneg  15759  lgsne0  15773  lgssq2  15776  lgsdirnn0  15782  gausslemma2dlem1a  15793  lgsquad  15815  2lgsoddprmlem2  15841  funvtxvalg  15893  funiedgvalg  15894  lpvtx  15936  upgrex  15960  subumgredg2en  16128  iedginwlk  16214  eulerpathprum  16337  gfsumsn  16711