Theorem simp1 1028

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  simpl1  1031  simpr1  1034  simp1i  1037  simp1d  1040  simp11  1058  simp21  1061  simp31  1064  syld3an3  1323  3ianorr  1350  intn3an1d  1397  stoic4a  1481  stoic4b  1482  rsp2e  2601  ifnetruedc  3684  issod  4462  elirr  4686  sotri2  5183  sotri3  5184  funtpg  5430  funimaexglem  5462  feq123  5523  ftpg  5893  fsnunf  5909  foco2  5953  fcofo  5984  f1oiso2  6027  riotass  6062  ovmpox  6211  ovmpoga  6212  caovimo  6277  ofeq  6299  ofrval  6307  fvn0elsuppb  6486  tfr1onlembxssdm  6608  tfrcllembxssdm  6621  frecsuclem  6671  frecrdg  6673  domssr  7058  mapxpen  7142  diffifi  7192  unsnfidcex  7221  unsnfidcel  7222  unfidisj  7223  undifdc  7225  ssfidc  7239  iunfidisj  7254  fissfi  7257  sbthlemi9  7276  elfir  7301  fdcf1  7310  djuassen  7567  dftap2  7611  mulcanenq  7746  ltanqg  7761  addnnnq0  7810  distrlem4prl  7945  distrlem4pru  7946  distrprg  7949  aptipr  8002  addsrpr  8106  mulsrpr  8107  mulasssrg  8119  ltpsrprg  8164  axmulass  8234  axpre-ltadd  8247  mul31  8451  addsubass  8530  subcan2  8545  subsub2  8548  subsub4  8553  npncan3  8558  pnpcan  8559  pnncan  8561  subcan  8575  subdi  8706  ltadd1  8751  leadd1  8752  leadd2  8753  ltsubadd  8754  lesubadd  8756  ltaddsub  8758  leaddsub  8760  lesub1  8778  lesub2  8779  ltsub1  8780  ltsub2  8781  ltaddsublt  8893  gt0add  8895  apreap  8909  lemul1  8915  reapmul1lem  8916  reapmul1  8917  reapadd1  8918  remulext1  8921  remulext2  8922  apadd2  8931  mulext2  8935  mulap0r  8937  leltap  8947  ltap  8955  apsub1  8964  recexaplem2  8974  mulcanap  8987  mulcanap2  8988  divvalap  8998  divcanap2  9004  diveqap0  9006  divrecap  9012  divrecap2  9013  divdirap  9021  divcanap3  9022  div11ap  9024  muldivdirap  9031  divcanap5  9038  redivclap  9055  div2negap  9059  apmul1  9112  apmul2  9113  div2subap  9161  ltdiv1  9192  ltmuldiv  9198  lemuldiv  9205  lt2msq1  9209  ltdiv23  9216  lediv23  9217  squeeze0  9228  ofnegsub  9286  difgtsumgt  9697  zfidc  9706  gtndiv  9724  eluz2  9910  eluzsub  9935  peano2uz  9966  nn01to3  10000  divge1  10107  ledivge1le  10110  addlelt  10152  xaddass  10254  xleadd1  10260  xltadd1  10261  ixxssixx  10287  lbico1  10315  lbicc2  10369  icoshftf1o  10376  fzen  10430  fzrev3  10477  fzrevral2  10496  nelfzo  10542  elfzo0  10576  elfzo0z  10579  fzosplitprm1  10636  qbtwnre  10674  flqwordi  10706  flqword2  10707  adddivflid  10710  flltdivnn0lt  10722  modqcl  10746  mulqmod0  10750  modqmulnn  10762  modqabs2  10778  addmodid  10792  modifeq2int  10806  modqeqmodmin  10814  seqeq2  10871  seqeq3  10872  seq1g  10883  seqp1g  10886  exp3val  10961  expnegap0  10967  expgt1  10997  exprecap  11000  leexp2a  11012  expubnd  11016  sqdivap  11023  expnbnd  11084  mulsubdivbinom2ap  11132  bccmpl  11175  fihashss  11240  leisorel  11272  ccatass  11359  ccats1val2  11391  swrdval  11403  swrdval2  11406  swrdlen2  11417  swrdfv2  11418  pfxfv  11439  pfxn0  11443  pfxnd  11444  swrdswrd  11460  pfxswrd  11461  pfxpfx  11463  ccats1pfxeqbi  11497  s3cl  11541  s3fv0g  11546  s3fv1g  11547  s3fv2g  11548  shftfibg  11568  mulreap  11612  abssubne0  11840  maxleast  11962  lemininf  11983  ltmininf  11984  xrmaxltsup  12007  xrmaxaddlem  12009  xrmaxadd  12010  xrmineqinf  12018  xrltmininf  12019  xrminltinf  12021  xrminadd  12024  climuni  12042  reccn2ap  12062  isumz  12139  fsumsplitsnun  12169  geoisum1c  12270  prod1dc  12336  efltim  12448  dvdscmulr  12570  dvdsmulcr  12571  summodnegmod  12572  modmulconst  12573  dvdsmultr2  12583  dvdsexp  12611  mulmoddvds  12613  modremain  12679  divgcdz  12731  gcdaddm  12744  dvdsgcdb  12773  gcdass  12775  mulgcd  12776  gcddiv  12779  rplpwr  12787  uzwodc  12797  lcmdvdsb  12845  lcmass  12846  mulgcddvds  12855  qredeq  12857  qredeu  12858  rpmul  12859  divgcdcoprmex  12863  cncongr1  12864  rpexp  12914  rpexp12i  12916  odzcllem  13004  odzdvds  13007  odzphi  13008  pythagtriplem15  13040  pcpremul  13055  pcdiv  13064  pcqmul  13065  pcqdiv  13069  dvdsprmpweq  13097  sumhashdc  13109  pcfaclem  13111  qexpz  13114  ballotfilemfrcn0  13256  ctinf  13304  setsvala  13366  ressressg  13412  ressabsg  13413  rngbaseg  13473  ptex  13601  issubmnd  13738  ress0g  13739  imasmnd2  13742  grpasscan2  13852  grpidrcan  13853  grpidlcan  13854  grpinvadd  13866  grpsubeq0  13874  grppncan  13879  dfgrp3m  13887  grpsubpropd2  13893  imasgrp2  13896  mhmmnd  13902  mulgnegneg  13927  mulgaddcomlem  13931  mulgaddcom  13932  mulginvcom  13933  mulgmodid  13947  issubg  13959  nsgconj  13992  nsgid  14001  quselbasg  14016  quseccl0g  14017  ghmnsgima  14054  cmn4  14091  ablinvadd  14097  ablsub4  14100  abladdsub4  14101  ablpncan2  14103  gsumsncmn  14139  gsumconstcmn  14149  pwsinvg  14198  rngpropd  14237  imasrng  14238  issrg  14252  ringidss  14317  ringcom  14319  imasring  14352  unitmulcl  14403  unitmulclb  14404  dvrcl  14425  unitdvcl  14426  dvrcan1  14430  dvrcan3  14431  issubrng  14490  subrngpropd  14507  rrgeq0  14556  islmod  14610  lmodcom  14653  rmodislmodlem  14670  rmodislmod  14671  lss0cl  14689  lssvnegcl  14696  lssintclm  14704  lssincl  14705  lspss  14719  lspun  14722  lspsnvsi  14738  lsslsp  14749  rnglidlmmgm  14816  rnglidlmsgrp  14817  rnglidlrng  14818  qus2idrng  14845  qusmulrng  14852  assa2ass  14992  assa2ass2  14993  aspid  15000  aspss  15002  asclmul1  15012  asclmul2  15013  asclinvg  15015  psrbaglecl  15043  psrbagcon  15045  2basgeng  15166  clsss  15202  ntrss  15203  ntrin  15208  neiss  15234  restco  15258  restabs  15259  lmconst  15300  psmetsym  15413  psmetge0  15415  xmetge0  15449  xmetsym  15452  xmetresbl  15524  mopni3  15568  bdxmet  15585  bdmopn  15588  txmetcnp  15602  dvfvalap  15765  dvid  15779  dvidre  15781  dvcnp2cntop  15783  elplyr  15824  ply1term  15827  ptolemy  15908  logfac  15978  rpcxpadd  15990  rpmulcxp  15994  rpdivcxp  15996  cxpmul  15997  rpcxple2  16003  rpcxplt2  16004  cxpcom  16023  rplogbval  16030  rplogbcl  16031  rprelogbmulexp  16041  relogbexpap  16043  logbleb  16046  logblt  16047  rplogbcxp  16048  rpcxplogb  16049  sgmppw  16089  lgslem1  16102  lgsfcl2  16108  lgsneg  16126  lgsne0  16140  lgssq2  16143  lgsdirnn0  16149  gausslemma2dlem1a  16160  lgsquad  16182  2lgsoddprmlem2  16208  funvtxvalg  16260  funiedgvalg  16261  lpvtx  16303  upgrex  16327  subumgredg2en  16495  iedginwlk  16581  eulerpathprum  16704  dichmul0or  16743