Theorem simp1 999

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  simpl1  1002  simpr1  1005  simp1i  1008  simp1d  1011  simp11  1029  simp21  1032  simp31  1035  syld3an3  1294  3ianorr  1320  stoic4a  1443  stoic4b  1444  rsp2e  2545  ifnetruedc  3598  issod  4350  elirr  4573  sotri2  5063  sotri3  5064  funtpg  5305  funimaexglem  5337  feq123  5395  ftpg  5742  fsnunf  5758  foco2  5796  fcofo  5827  f1oiso2  5870  riotass  5901  ovmpox  6047  ovmpoga  6048  caovimo  6112  ofeq  6133  ofrval  6141  tfr1onlembxssdm  6396  tfrcllembxssdm  6409  frecsuclem  6459  frecrdg  6461  mapxpen  6904  diffifi  6950  unsnfidcex  6976  unsnfidcel  6977  unfidisj  6978  undifdc  6980  ssfidc  6991  iunfidisj  7005  sbthlemi9  7024  elfir  7032  djuassen  7277  dftap2  7311  mulcanenq  7445  ltanqg  7460  addnnnq0  7509  distrlem4prl  7644  distrlem4pru  7645  distrprg  7648  aptipr  7701  addsrpr  7805  mulsrpr  7806  mulasssrg  7818  ltpsrprg  7863  axmulass  7933  axpre-ltadd  7946  mul31  8150  addsubass  8229  subcan2  8244  subsub2  8247  subsub4  8252  npncan3  8257  pnpcan  8258  pnncan  8260  subcan  8274  subdi  8404  ltadd1  8448  leadd1  8449  leadd2  8450  ltsubadd  8451  lesubadd  8453  ltaddsub  8455  leaddsub  8457  lesub1  8475  lesub2  8476  ltsub1  8477  ltsub2  8478  ltaddsublt  8590  gt0add  8592  apreap  8606  lemul1  8612  reapmul1lem  8613  reapmul1  8614  reapadd1  8615  remulext1  8618  remulext2  8619  apadd2  8628  mulext2  8632  mulap0r  8634  leltap  8644  ltap  8652  apsub1  8661  recexaplem2  8671  mulcanap  8684  mulcanap2  8685  divvalap  8693  divcanap2  8699  diveqap0  8701  divrecap  8707  divrecap2  8708  divdirap  8716  divcanap3  8717  div11ap  8719  muldivdirap  8726  divcanap5  8733  redivclap  8750  div2negap  8754  apmul1  8807  apmul2  8808  div2subap  8856  ltdiv1  8887  ltmuldiv  8893  lemuldiv  8900  lt2msq1  8904  ltdiv23  8911  lediv23  8912  squeeze0  8923  ofnegsub  8981  difgtsumgt  9386  gtndiv  9412  eluz2  9598  eluzsub  9622  peano2uz  9648  nn01to3  9682  divge1  9789  ledivge1le  9792  addlelt  9834  xaddass  9935  xleadd1  9941  xltadd1  9942  ixxssixx  9968  lbico1  9996  lbicc2  10050  icoshftf1o  10057  fzen  10109  fzrev3  10153  fzrevral2  10172  nelfzo  10218  elfzo0  10249  elfzo0z  10251  fzosplitprm1  10301  qbtwnre  10325  flqwordi  10357  flqword2  10358  adddivflid  10361  flltdivnn0lt  10373  modqcl  10397  mulqmod0  10401  modqmulnn  10413  modqabs2  10429  addmodid  10443  modifeq2int  10457  modqeqmodmin  10465  seqeq2  10522  seqeq3  10523  seq1g  10534  seqp1g  10537  exp3val  10612  expnegap0  10618  expgt1  10648  exprecap  10651  leexp2a  10663  expubnd  10667  sqdivap  10674  expnbnd  10734  mulsubdivbinom2ap  10782  bccmpl  10825  fihashss  10887  leisorel  10908  shftfibg  10964  mulreap  11008  abssubne0  11235  maxleast  11357  lemininf  11377  ltmininf  11378  xrmaxltsup  11401  xrmaxaddlem  11403  xrmaxadd  11404  xrmineqinf  11412  xrltmininf  11413  xrminltinf  11415  xrminadd  11418  climuni  11436  reccn2ap  11456  isumz  11532  fsumsplitsnun  11562  geoisum1c  11663  prod1dc  11729  efltim  11841  dvdscmulr  11963  dvdsmulcr  11964  summodnegmod  11965  modmulconst  11966  dvdsmultr2  11976  dvdsexp  12003  mulmoddvds  12005  modremain  12070  divgcdz  12108  gcdaddm  12121  dvdsgcdb  12150  gcdass  12152  mulgcd  12153  gcddiv  12156  rplpwr  12164  uzwodc  12174  lcmdvdsb  12222  lcmass  12223  mulgcddvds  12232  qredeq  12234  qredeu  12235  rpmul  12236  divgcdcoprmex  12240  cncongr1  12241  rpexp  12291  rpexp12i  12293  odzcllem  12380  odzdvds  12383  odzphi  12384  pythagtriplem15  12416  pcpremul  12431  pcdiv  12440  pcqmul  12441  pcqdiv  12445  dvdsprmpweq  12473  sumhashdc  12485  pcfaclem  12487  qexpz  12490  ctinf  12587  setsvala  12649  ressressg  12693  ressabsg  12694  rngbaseg  12753  ptex  12875  issubmnd  13023  ress0g  13024  gsumfzz  13067  grpasscan2  13136  grpidrcan  13137  grpidlcan  13138  grpinvadd  13150  grpsubeq0  13158  grppncan  13163  dfgrp3m  13171  grpsubpropd2  13177  imasgrp2  13180  mhmmnd  13186  mulgnegneg  13211  mulgaddcomlem  13215  mulgaddcom  13216  mulginvcom  13217  mulgmodid  13231  issubg  13243  nsgconj  13276  nsgid  13285  quselbasg  13300  quseccl0g  13301  ghmnsgima  13338  cmn4  13375  ablinvadd  13380  ablsub4  13383  abladdsub4  13384  ablpncan2  13386  rngpropd  13451  imasrng  13452  issrg  13461  ringidss  13525  ringcom  13527  imasring  13560  unitmulcl  13609  unitmulclb  13610  dvrcl  13631  unitdvcl  13632  dvrcan1  13636  dvrcan3  13637  issubrng  13695  subrngpropd  13712  rrgeq0  13761  islmod  13787  lmodcom  13829  rmodislmodlem  13846  rmodislmod  13847  lss0cl  13865  lssvnegcl  13872  lssintclm  13880  lssincl  13881  lspss  13895  lspun  13898  lspsnvsi  13914  lsslsp  13925  rnglidlmmgm  13992  rnglidlmsgrp  13993  rnglidlrng  13994  qus2idrng  14021  qusmulrng  14028  2basgeng  14250  clsss  14286  ntrss  14287  ntrin  14292  neiss  14318  restco  14342  restabs  14343  lmconst  14384  psmetsym  14497  psmetge0  14499  xmetge0  14533  xmetsym  14536  xmetresbl  14608  mopni3  14652  bdxmet  14669  bdmopn  14672  txmetcnp  14686  dvfvalap  14835  dvid  14847  dvcnp2cntop  14848  elplyr  14886  ply1term  14889  ptolemy  14959  rpcxpadd  15040  rpmulcxp  15044  rpdivcxp  15046  cxpmul  15047  rpcxple2  15052  rpcxplt2  15053  cxpcom  15071  rplogbval  15077  rplogbcl  15078  rprelogbmulexp  15088  relogbexpap  15090  logbleb  15093  logblt  15094  rplogbcxp  15095  rpcxplogb  15096  lgslem1  15116  lgsfcl2  15122  lgsneg  15140  lgsne0  15154  lgssq2  15157  lgsdirnn0  15163  gausslemma2dlem1a  15174  2lgsoddprmlem2  15194