Theorem simp3 1030

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 1027	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 114	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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  simpl3  1033  simpr3  1036  simp3i  1039  simp3d  1042  simp13  1060  simp23  1063  simp33  1066  3anibar  1196  3ianorr  1350  intn3an3d  1399  stoic4a  1481  stoic4b  1482  mob2  3006  sotri2  5183  sotri3  5184  feq123  5523  resasplitss  5567  fresaunres2disj  5568  sefvex  5714  ftpg  5893  fsnunf  5909  fnfvima  5947  cocan1  5987  cocan2  5988  f1oiso2  6027  riotass  6062  moriotass  6063  ovmpox  6211  ovmpoga  6212  fvmpopr2d  6219  caovimo  6277  ofrval  6307  suppvalfn  6475  fvn0elsuppb  6486  dfsmo2  6552  tfr1onlembfn  6609  tfrcllembfn  6622  freccllem  6667  frecfcllem  6669  frecsuclem  6671  frecrdg  6673  nnsucsssuc  6759  f1oen2g  7035  f1dom2g  7036  xpdom3m  7126  mapxpen  7142  diffifi  7192  unfidisj  7223  undifdc  7225  imaf1fi  7234  ssfidc  7239  sbthlemi9  7276  fdcf1  7310  ctssdc  7447  endjudisj  7560  djuassen  7567  xpdjuen  7568  mulcanenq  7746  ltanqg  7761  addnnnq0  7810  nnanq0  7819  prltlu  7848  distrprg  7949  ltexprlemm  7961  recexprlem1ssl  7994  recexprlem1ssu  7995  addsrpr  8106  mulsrpr  8107  mulasssrg  8119  recexgt0sr  8134  ltpsrprg  8164  axmulass  8234  axpre-ltadd  8247  ltxrlt  8385  subadd2  8524  addsubass  8530  nppcan  8542  nppcan3  8544  subcan2  8545  subsub2  8548  subsub4  8553  pnpcan  8559  pnncan  8561  subcan  8575  subdi  8706  ltadd1  8751  leadd1  8752  leadd2  8753  ltsubadd  8754  ltsubadd2  8755  lesubadd  8756  lesubadd2  8757  ltaddsub  8758  leaddsub  8760  lesub1  8778  lesub2  8779  ltsub1  8780  ltsub2  8781  ltaddsublt  8893  gt0add  8895  reapadd1  8918  remulext1  8921  remulext2  8922  apadd2  8931  mulext2  8935  mulap0r  8937  leltap  8947  ltap  8955  apsub1  8964  divap0b  9007  divmulasscomap  9020  divcanap5  9038  dmdcanap  9046  redivclap  9055  div2negap  9059  lt2msq1  9209  ltdiv2  9211  ofnegsub  9286  nndivtr  9329  difgtsumgt  9697  zfidc  9706  gtndiv  9724  eluzsub  9935  nn01to3  10000  qdivcl  10026  irrmul  10030  rpgecl  10066  divge1  10107  xaddass  10254  xltadd1  10261  ubioog  10299  ubioc1  10314  lbico1  10315  iccleub  10316  lbicc2  10369  ubicc2  10370  icoshftf1o  10376  fzen  10430  elfz1b  10480  uznfz  10493  elfzo0  10576  elfzo0z  10579  ubmelfzo  10601  fzonn0p1p1  10614  ubmelm1fzo  10627  zsupssdc  10656  qbtwnre  10674  flqwordi  10706  flltdivnn0lt  10722  ceiqle  10733  modqval  10744  modqvalr  10745  modqcl  10746  flqpmodeq  10747  modq0  10749  mulqmod0  10750  negqmod0  10751  modqge0  10752  modqlt  10753  modqdiffl  10755  modqdifz  10756  modqmulnn  10762  modqvalp1  10763  modqabs2  10778  modqmuladdnn0  10788  qnegmod  10789  addmodid  10792  modqeqmodmin  10814  modfzo0difsn  10815  addmodlteq  10818  frec2uzf1od  10826  expnegap0  10967  expgt1  10997  exprecap  11000  expaddzaplem  11002  expaddzap  11003  expmulzap  11005  mulbinom2  11076  expnbnd  11084  fihashss  11240  fimaxq  11253  seq3coll  11277  ccatw2s1leng  11389  ccat2s1fvwd  11398  swrdval  11403  swrdnd  11414  swrdlen2  11417  pfxn0  11443  ccatopth2  11472  s3cl  11541  s3fv0g  11546  s3fv1g  11547  s3fv2g  11548  shftfibg  11568  redivap  11622  imdivap  11629  cjdivap  11658  maxleast  11962  lemininf  11983  ltmininf  11984  bdtrilem  11988  bdtri  11989  xrmaxaddlem  12009  xrmaxadd  12010  xrmineqinf  12018  xrltmininf  12019  xrminltinf  12021  xrminadd  12024  climuni  12042  reccn2ap  12062  isumz  12139  fsumsplitsnun  12169  geoisum1c  12270  prodfap0  12295  prod1dc  12336  fprodabs  12366  cos12dec  12518  summodnegmod  12572  dvdsmultr2  12583  mulmoddvds  12613  divalglemeuneg  12673  gcdaddm  12744  gcdass  12775  mulgcd  12776  gcddiv  12779  nnminle  12795  lcmass  12846  mulgcddvds  12855  qredeq  12857  congr  12861  divgcdcoprmex  12863  cncongr1  12864  cncongr2  12865  prmexpb  12912  rpexp  12914  pythagtriplem1  13027  pythagtriplem6  13032  pythagtriplem7  13033  pythagtriplem12  13037  pythagtriplem13  13038  pythagtriplem15  13040  pythagtriplem19  13044  pcdiv  13064  dvdsprmpweqle  13099  sumhashdc  13109  pcbc  13113  4sqlem12  13164  4sqlem18  13170  ballotfilemsgt1  13237  ballotfilemfrcn0  13256  unennn  13271  nninfdc  13327  fvsetsid  13369  ressressg  13412  rngmulrg  13475  imasaddvallemg  13619  qusaddvallemg  13637  mgmsscl  13664  plusfvalg  13666  ress0g  13739  imasmnd2  13742  imasmnd  13743  grpasscan2  13852  grpidrcan  13853  grpidlcan  13854  grpinvadd  13866  grppncan  13879  dfgrp3me  13888  grpsubpropd2  13893  imasgrp2  13896  imasgrp  13897  mhmmnd  13902  mulgnnsubcl  13920  mulgnn0subcl  13921  mulgsubcl  13922  mulgaddcomlem  13931  mulgaddcom  13932  mulgpropdg  13950  submmulg  13952  subgcl  13970  subgsubcl  13971  subgsub  13972  subgmulg  13974  nsgconj  13992  ghmsub  14037  ghmnsgima  14054  ghmeqker  14057  f1ghm0to0  14058  ablinvadd  14097  ablpncan2  14103  subgabl  14119  gsumsncmn  14139  gsumconstcmn  14149  pwsinvg  14198  rngcl  14226  imasrng  14238  rng1zrlem  14241  srgcl  14257  ringcl  14300  crngcom  14301  ringidss  14317  ringcom  14319  mulgass2  14346  imasring  14352  opprringbg  14368  unitmulcl  14403  unitmulclb  14404  dvrcl  14425  unitdvcl  14426  dvrcan1  14430  dvrcan3  14431  rhmmul  14454  subrngmcl  14500  subrgmcl  14524  subrgdv  14529  domneq0  14564  islmod  14610  scafvalg  14627  lmodcom  14653  lmodprop2d  14668  rmodislmodlem  14670  rmodislmod  14671  lsselg  14681  lssvnegcl  14696  lspss  14719  lspun  14722  lspsnvsi  14738  lsslsp  14749  sralmod  14770  lidlnegcl  14805  rspssp  14814  rnglidlrng  14818  qus2idrng  14845  zndvds  14967  aspss  15002  asclmul1  15012  asclmul2  15013  ascldimul  15014  asclinvg  15015  asclmulg  15027  psrbagaddclfi  15044  psrbagcon  15045  basgen  15164  2basgeng  15166  ntrss  15203  neiss  15234  opnneiss  15242  restco  15258  restabs  15259  cnprcl2k  15290  cnpf2  15291  lmconst  15300  cnpnei  15303  cnptoprest  15323  cnmpt2t  15377  psmetsym  15413  psmetge0  15415  xmetge0  15449  xmetsym  15452  blvalps  15472  blval  15473  ssblps  15509  ssbl  15510  blpnfctr  15523  xmssym  15553  bdxmet  15585  metcnp3  15595  dvfvalap  15765  dvid  15779  dvidre  15781  dvcnp2cntop  15783  elplyr  15824  ply1term  15827  plypow  15828  ptolemy  15908  logfac  15978  rpcxpadd  15990  rpcxpsub  15993  rpmulcxp  15994  cxpmul  15997  rpcxple2  16003  rpcxplt2  16004  cxpcom  16023  rplogbval  16030  rplogbcl  16031  rplogbchbase  16035  rplogbreexp  16038  relogbexpap  16043  logbleb  16046  logblt  16047  rplogbcxp  16048  rpcxplogb  16049  relogbcxpbap  16050  sgmppw  16089  lgslem1  16102  lgsfvalg  16107  lgsval4  16122  lgsneg  16126  lgsne0  16140  lgsdinn0  16150  lgsquad  16182  funvtxvalg  16260  funiedgvalg  16261  upgrex  16327  uhgr2edg  16430  usgr2v1e2w  16470  subumgredg2en  16495  iedginwlk  16581  upgrwlkedg  16585  clwwlkccat  16625  clwwlknonex2  16663  eulerpathprum  16704  dichmul0or  16743  repiecele0  17049  repiecege0  17050