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  2584  ifnetruedc  3653  issod  4422  elirr  4645  sotri2  5141  sotri3  5142  funtpg  5388  funimaexglem  5420  feq123  5481  ftpg  5846  fsnunf  5862  foco2  5904  fcofo  5935  f1oiso2  5978  riotass  6011  ovmpox  6160  ovmpoga  6161  caovimo  6226  ofeq  6247  ofrval  6255  fvn0elsuppb  6430  tfr1onlembxssdm  6552  tfrcllembxssdm  6565  frecsuclem  6615  frecrdg  6617  domssr  6994  mapxpen  7077  diffifi  7126  unsnfidcex  7155  unsnfidcel  7156  unfidisj  7157  undifdc  7159  ssfidc  7173  iunfidisj  7188  sbthlemi9  7207  elfir  7215  djuassen  7475  dftap2  7513  mulcanenq  7648  ltanqg  7663  addnnnq0  7712  distrlem4prl  7847  distrlem4pru  7848  distrprg  7851  aptipr  7904  addsrpr  8008  mulsrpr  8009  mulasssrg  8021  ltpsrprg  8066  axmulass  8136  axpre-ltadd  8149  mul31  8352  addsubass  8431  subcan2  8446  subsub2  8449  subsub4  8454  npncan3  8459  pnpcan  8460  pnncan  8462  subcan  8476  subdi  8606  ltadd1  8651  leadd1  8652  leadd2  8653  ltsubadd  8654  lesubadd  8656  ltaddsub  8658  leaddsub  8660  lesub1  8678  lesub2  8679  ltsub1  8680  ltsub2  8681  ltaddsublt  8793  gt0add  8795  apreap  8809  lemul1  8815  reapmul1lem  8816  reapmul1  8817  reapadd1  8818  remulext1  8821  remulext2  8822  apadd2  8831  mulext2  8835  mulap0r  8837  leltap  8847  ltap  8855  apsub1  8864  recexaplem2  8874  mulcanap  8887  mulcanap2  8888  divvalap  8896  divcanap2  8902  diveqap0  8904  divrecap  8910  divrecap2  8911  divdirap  8919  divcanap3  8920  div11ap  8922  muldivdirap  8929  divcanap5  8936  redivclap  8953  div2negap  8957  apmul1  9010  apmul2  9011  div2subap  9059  ltdiv1  9090  ltmuldiv  9096  lemuldiv  9103  lt2msq1  9107  ltdiv23  9114  lediv23  9115  squeeze0  9126  ofnegsub  9184  difgtsumgt  9593  gtndiv  9619  eluz2  9805  eluzsub  9830  peano2uz  9861  nn01to3  9895  divge1  10002  ledivge1le  10005  addlelt  10047  xaddass  10148  xleadd1  10154  xltadd1  10155  ixxssixx  10181  lbico1  10209  lbicc2  10263  icoshftf1o  10270  fzen  10323  fzrev3  10367  fzrevral2  10386  nelfzo  10432  elfzo0  10466  elfzo0z  10469  fzosplitprm1  10526  qbtwnre  10562  flqwordi  10594  flqword2  10595  adddivflid  10598  flltdivnn0lt  10610  modqcl  10634  mulqmod0  10638  modqmulnn  10650  modqabs2  10666  addmodid  10680  modifeq2int  10694  modqeqmodmin  10702  seqeq2  10759  seqeq3  10760  seq1g  10771  seqp1g  10774  exp3val  10849  expnegap0  10855  expgt1  10885  exprecap  10888  leexp2a  10900  expubnd  10904  sqdivap  10911  expnbnd  10971  mulsubdivbinom2ap  11019  bccmpl  11062  fihashss  11126  leisorel  11147  ccatass  11234  ccats1val2  11266  swrdval  11278  swrdval2  11281  swrdlen2  11292  swrdfv2  11293  pfxfv  11314  pfxn0  11318  pfxnd  11319  swrdswrd  11335  pfxswrd  11336  pfxpfx  11338  ccats1pfxeqbi  11372  s3cl  11416  s3fv0g  11421  s3fv1g  11422  s3fv2g  11423  shftfibg  11443  mulreap  11487  abssubne0  11714  maxleast  11836  lemininf  11857  ltmininf  11858  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  xrmineqinf  11892  xrltmininf  11893  xrminltinf  11895  xrminadd  11898  climuni  11916  reccn2ap  11936  isumz  12013  fsumsplitsnun  12043  geoisum1c  12144  prod1dc  12210  efltim  12322  dvdscmulr  12444  dvdsmulcr  12445  summodnegmod  12446  modmulconst  12447  dvdsmultr2  12457  dvdsexp  12485  mulmoddvds  12487  modremain  12553  divgcdz  12605  gcdaddm  12618  dvdsgcdb  12647  gcdass  12649  mulgcd  12650  gcddiv  12653  rplpwr  12661  uzwodc  12671  lcmdvdsb  12719  lcmass  12720  mulgcddvds  12729  qredeq  12731  qredeu  12732  rpmul  12733  divgcdcoprmex  12737  cncongr1  12738  rpexp  12788  rpexp12i  12790  odzcllem  12878  odzdvds  12881  odzphi  12882  pythagtriplem15  12914  pcpremul  12929  pcdiv  12938  pcqmul  12939  pcqdiv  12943  dvdsprmpweq  12971  sumhashdc  12983  pcfaclem  12985  qexpz  12988  ctinf  13114  setsvala  13176  ressressg  13221  ressabsg  13222  rngbaseg  13282  ptex  13410  issubmnd  13588  ress0g  13589  imasmnd2  13598  gsumfzz  13641  grpasscan2  13710  grpidrcan  13711  grpidlcan  13712  grpinvadd  13724  grpsubeq0  13732  grppncan  13737  dfgrp3m  13745  grpsubpropd2  13751  pwsinvg  13758  imasgrp2  13760  mhmmnd  13766  mulgnegneg  13791  mulgaddcomlem  13795  mulgaddcom  13796  mulginvcom  13797  mulgmodid  13811  issubg  13823  nsgconj  13856  nsgid  13865  quselbasg  13880  quseccl0g  13881  ghmnsgima  13918  cmn4  13955  ablinvadd  13960  ablsub4  13963  abladdsub4  13964  ablpncan2  13966  rngpropd  14032  imasrng  14033  issrg  14042  ringidss  14106  ringcom  14108  imasring  14141  unitmulcl  14191  unitmulclb  14192  dvrcl  14213  unitdvcl  14214  dvrcan1  14218  dvrcan3  14219  issubrng  14277  subrngpropd  14294  rrgeq0  14343  islmod  14370  lmodcom  14412  rmodislmodlem  14429  rmodislmod  14430  lss0cl  14448  lssvnegcl  14455  lssintclm  14463  lssincl  14464  lspss  14478  lspun  14481  lspsnvsi  14497  lsslsp  14508  rnglidlmmgm  14575  rnglidlmsgrp  14576  rnglidlrng  14577  qus2idrng  14604  qusmulrng  14611  psrbaglecl  14754  psrbagcon  14755  2basgeng  14876  clsss  14912  ntrss  14913  ntrin  14918  neiss  14944  restco  14968  restabs  14969  lmconst  15010  psmetsym  15123  psmetge0  15125  xmetge0  15159  xmetsym  15162  xmetresbl  15234  mopni3  15278  bdxmet  15295  bdmopn  15298  txmetcnp  15312  dvfvalap  15475  dvid  15489  dvidre  15491  dvcnp2cntop  15493  elplyr  15534  ply1term  15537  ptolemy  15618  rpcxpadd  15699  rpmulcxp  15703  rpdivcxp  15705  cxpmul  15706  rpcxple2  15712  rpcxplt2  15713  cxpcom  15732  rplogbval  15739  rplogbcl  15740  rprelogbmulexp  15750  relogbexpap  15752  logbleb  15755  logblt  15756  rplogbcxp  15757  rpcxplogb  15758  sgmppw  15789  lgslem1  15802  lgsfcl2  15808  lgsneg  15826  lgsne0  15840  lgssq2  15843  lgsdirnn0  15849  gausslemma2dlem1a  15860  lgsquad  15882  2lgsoddprmlem2  15908  funvtxvalg  15960  funiedgvalg  15961  lpvtx  16003  upgrex  16027  subumgredg2en  16195  iedginwlk  16281  eulerpathprum  16404  gfsumsn  16797