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  8421  addsubass  8500  subcan2  8515  subsub2  8518  subsub4  8523  npncan3  8528  pnpcan  8529  pnncan  8531  subcan  8545  subdi  8676  ltadd1  8721  leadd1  8722  leadd2  8723  ltsubadd  8724  lesubadd  8726  ltaddsub  8728  leaddsub  8730  lesub1  8748  lesub2  8749  ltsub1  8750  ltsub2  8751  ltaddsublt  8863  gt0add  8865  apreap  8879  lemul1  8885  reapmul1lem  8886  reapmul1  8887  reapadd1  8888  remulext1  8891  remulext2  8892  apadd2  8901  mulext2  8905  mulap0r  8907  leltap  8917  ltap  8925  apsub1  8934  recexaplem2  8944  mulcanap  8957  mulcanap2  8958  divvalap  8968  divcanap2  8974  diveqap0  8976  divrecap  8982  divrecap2  8983  divdirap  8991  divcanap3  8992  div11ap  8994  muldivdirap  9001  divcanap5  9008  redivclap  9025  div2negap  9029  apmul1  9082  apmul2  9083  div2subap  9131  ltdiv1  9162  ltmuldiv  9168  lemuldiv  9175  lt2msq1  9179  ltdiv23  9186  lediv23  9187  squeeze0  9198  ofnegsub  9256  difgtsumgt  9667  zfidc  9676  gtndiv  9694  eluz2  9880  eluzsub  9905  peano2uz  9936  nn01to3  9970  divge1  10077  ledivge1le  10080  addlelt  10122  xaddass  10224  xleadd1  10230  xltadd1  10231  ixxssixx  10257  lbico1  10285  lbicc2  10339  icoshftf1o  10346  fzen  10400  fzrev3  10446  fzrevral2  10465  nelfzo  10511  elfzo0  10545  elfzo0z  10548  fzosplitprm1  10605  qbtwnre  10643  flqwordi  10675  flqword2  10676  adddivflid  10679  flltdivnn0lt  10691  modqcl  10715  mulqmod0  10719  modqmulnn  10731  modqabs2  10747  addmodid  10761  modifeq2int  10775  modqeqmodmin  10783  seqeq2  10840  seqeq3  10841  seq1g  10852  seqp1g  10855  exp3val  10930  expnegap0  10936  expgt1  10966  exprecap  10969  leexp2a  10981  expubnd  10985  sqdivap  10992  expnbnd  11053  mulsubdivbinom2ap  11101  bccmpl  11144  fihashss  11209  leisorel  11237  ccatass  11324  ccats1val2  11356  swrdval  11368  swrdval2  11371  swrdlen2  11382  swrdfv2  11383  pfxfv  11404  pfxn0  11408  pfxnd  11409  swrdswrd  11425  pfxswrd  11426  pfxpfx  11428  ccats1pfxeqbi  11462  s3cl  11506  s3fv0g  11511  s3fv1g  11512  s3fv2g  11513  shftfibg  11533  mulreap  11577  abssubne0  11805  maxleast  11927  lemininf  11948  ltmininf  11949  xrmaxltsup  11972  xrmaxaddlem  11974  xrmaxadd  11975  xrmineqinf  11983  xrltmininf  11984  xrminltinf  11986  xrminadd  11989  climuni  12007  reccn2ap  12027  isumz  12104  fsumsplitsnun  12134  geoisum1c  12235  prod1dc  12301  efltim  12413  dvdscmulr  12535  dvdsmulcr  12536  summodnegmod  12537  modmulconst  12538  dvdsmultr2  12548  dvdsexp  12576  mulmoddvds  12578  modremain  12644  divgcdz  12696  gcdaddm  12709  dvdsgcdb  12738  gcdass  12740  mulgcd  12741  gcddiv  12744  rplpwr  12752  uzwodc  12762  lcmdvdsb  12810  lcmass  12811  mulgcddvds  12820  qredeq  12822  qredeu  12823  rpmul  12824  divgcdcoprmex  12828  cncongr1  12829  rpexp  12879  rpexp12i  12881  odzcllem  12969  odzdvds  12972  odzphi  12973  pythagtriplem15  13005  pcpremul  13020  pcdiv  13029  pcqmul  13030  pcqdiv  13034  dvdsprmpweq  13062  sumhashdc  13074  pcfaclem  13076  qexpz  13079  ballotfilemfrcn0  13221  ctinf  13269  setsvala  13331  ressressg  13376  ressabsg  13377  rngbaseg  13437  ptex  13565  issubmnd  13707  ress0g  13708  imasmnd2  13711  gsumfzz  13754  grpasscan2  13823  grpidrcan  13824  grpidlcan  13825  grpinvadd  13837  grpsubeq0  13845  grppncan  13850  dfgrp3m  13858  grpsubpropd2  13864  imasgrp2  13867  mhmmnd  13873  mulgnegneg  13898  mulgaddcomlem  13902  mulgaddcom  13903  mulginvcom  13904  mulgmodid  13918  issubg  13930  nsgconj  13963  nsgid  13972  quselbasg  13987  quseccl0g  13988  ghmnsgima  14025  cmn4  14062  ablinvadd  14067  ablsub4  14070  abladdsub4  14071  ablpncan2  14073  gfsumsn  14111  pwsinvg  14161  rngpropd  14198  imasrng  14199  issrg  14212  ringidss  14276  ringcom  14278  imasring  14311  unitmulcl  14362  unitmulclb  14363  dvrcl  14384  unitdvcl  14385  dvrcan1  14389  dvrcan3  14390  issubrng  14449  subrngpropd  14466  rrgeq0  14515  islmod  14569  lmodcom  14611  rmodislmodlem  14628  rmodislmod  14629  lss0cl  14647  lssvnegcl  14654  lssintclm  14662  lssincl  14663  lspss  14677  lspun  14680  lspsnvsi  14696  lsslsp  14707  rnglidlmmgm  14774  rnglidlmsgrp  14775  rnglidlrng  14776  qus2idrng  14803  qusmulrng  14810  psrbaglecl  14954  psrbagcon  14956  2basgeng  15077  clsss  15113  ntrss  15114  ntrin  15119  neiss  15145  restco  15169  restabs  15170  lmconst  15211  psmetsym  15324  psmetge0  15326  xmetge0  15360  xmetsym  15363  xmetresbl  15435  mopni3  15479  bdxmet  15496  bdmopn  15499  txmetcnp  15513  dvfvalap  15676  dvid  15690  dvidre  15692  dvcnp2cntop  15694  elplyr  15735  ply1term  15738  ptolemy  15819  rpcxpadd  15900  rpmulcxp  15904  rpdivcxp  15906  cxpmul  15907  rpcxple2  15913  rpcxplt2  15914  cxpcom  15933  rplogbval  15940  rplogbcl  15941  rprelogbmulexp  15951  relogbexpap  15953  logbleb  15956  logblt  15957  rplogbcxp  15958  rpcxplogb  15959  sgmppw  15990  lgslem1  16003  lgsfcl2  16009  lgsneg  16027  lgsne0  16041  lgssq2  16044  lgsdirnn0  16050  gausslemma2dlem1a  16061  lgsquad  16083  2lgsoddprmlem2  16109  funvtxvalg  16161  funiedgvalg  16162  lpvtx  16204  upgrex  16228  subumgredg2en  16396  iedginwlk  16482  eulerpathprum  16605  dichmul0or  16644