Theorem simp2 1029

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

Assertion

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

Proof of Theorem simp2

Step	Hyp	Ref	Expression
1		3simpa 1025	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜑 ∧ 𝜓))
2	1	simprd 114	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

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

This theorem is used by:  simpl2  1032  simpr2  1035  simp2i  1038  simp2d  1041  simp12  1059  simp22  1062  simp32  1065  syld3an3  1323  3ianorr  1350  intn3an2d  1398  stoic4b  1482  nlim0  4539  tfisi  4734  sotri2  5185  sotri3  5186  feq123  5525  sefvex  5716  fvmptt  5797  fnfvima  5953  cocan1  5993  cocan2  5994  ovexg  6119  ovmpox  6217  ovmpoga  6218  fvmpopr2d  6225  caovimo  6283  suppval1  6479  suppimacnvfn  6486  suppfnss  6497  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfrcllembxssdm  6627  tfrcllembfn  6628  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  domssr  7064  mapxpen  7148  dif1en  7183  diffifi  7198  unsnfidcex  7227  unfidisj  7229  undifdc  7231  resfnfinfinss  7253  funrnfi  7256  fissfi  7263  sbthlemi9  7282  elfir  7307  difinfsn  7440  ctssdc  7453  djuassen  7573  xpdjuen  7574  mulcanenq  7752  ltanqg  7767  mulcanenq0ec  7812  addnnnq0  7816  distrprg  7955  aptipr  8008  addsrpr  8112  mulsrpr  8113  mulasssrg  8125  ltpsrprg  8170  axmulass  8240  axpre-ltadd  8253  subadd2  8530  nppcan  8548  nppcan3  8550  subsub2  8554  subsub4  8559  npncan3  8564  pnpcan  8565  pnncan  8567  subcan  8581  ltadd1  8757  leadd1  8758  leadd2  8759  ltsubadd  8760  ltsubadd2  8761  lesubadd  8762  lesubadd2  8763  ltaddsub  8764  leaddsub  8766  lesub1  8784  lesub2  8785  ltsub1  8786  ltsub2  8787  gt0add  8902  apreap  8916  lemul1  8922  reapmul1lem  8923  reapmul1  8924  reapadd1  8925  remulext1  8928  remulext2  8929  apadd2  8938  mulext2  8942  mulap0r  8944  leltap  8954  ltap  8962  apsub1  8971  recexaplem2  8981  mulcanap  8994  mulcanap2  8995  divvalap  9005  divmulap  9006  divcanap1  9012  diveqap0  9013  divap0b  9014  divrecap  9019  divassap  9021  div23ap  9022  divdirap  9028  divcanap3  9029  div11ap  9031  diveqap1  9036  divmuldivap  9043  divcanap5  9045  redivclap  9062  div2negap  9066  apmul1  9119  apmul2  9120  div2subap  9168  ltdiv1  9199  ledivmul  9208  lemuldiv  9212  lt2msq1  9216  ltdiv23  9223  squeeze0  9235  ofnegsub  9293  ind1  9301  zaddcllemneg  9685  zfidc  9725  eluzsub  9954  nn01to3  10019  rpgecl  10085  addlelt  10171  xleadd1  10279  xltadd1  10280  lbioog  10317  ubioc1  10333  ubicc2  10389  icoshftf1o  10395  fzen  10449  nelfzo  10561  ubmelfzo  10620  ssfzo12  10644  ubmelm1fzo  10646  fzosplitprm1  10655  zsupssdc  10675  rebtwn2zlemshrink  10690  qbtwnre  10693  icogelb  10702  flqwordi  10725  flqword2  10726  flltdivnn0lt  10741  modqcl  10765  mulqmod0  10769  modqmulnn  10781  modqabs2  10797  modqmuladdnn0  10807  qnegmod  10808  addmodid  10811  modqm1p1mod0  10814  modifeq2int  10825  modqdi  10831  modqeqmodmin  10833  modfzo0difsn  10834  frec2uzf1od  10845  exp3val  10980  expnegap0  10986  expgt1  11016  exprecap  11019  expmulzap  11024  leexp2a  11031  expubnd  11035  mulbinom2  11095  bernneq2  11101  expnbnd  11103  fihashss  11259  fihashssdif  11261  fimaxq  11272  ccatval2  11368  ccatass  11378  ccatw2s1leng  11408  ccat2s1fvwd  11417  swrdval  11422  swrdnd  11433  pfxfv  11458  pfxpfx  11482  ccats1pfxeq  11488  ccats1pfxeqrex  11489  s3cl  11560  s3fv0g  11565  s3fv1g  11566  s3fv2g  11567  shftuz  11584  shftfibg  11587  cjdivap  11677  resqrtcl  11797  absdivap  11838  abssubne0  11859  maxleast  11981  lemininf  12002  ltmininf  12003  xrmaxltsup  12026  xrmaxaddlem  12028  xrmaxadd  12029  xrmineqinf  12037  xrltmininf  12038  xrminltinf  12040  xrminadd  12043  climuni  12061  reccn2ap  12081  isumz  12158  geoisum1c  12289  prod1dc  12355  efltim  12467  dvdsval2  12559  dvdscmulr  12589  dvdsmulcr  12590  modmulconst  12592  dvdsadd2b  12609  dvdsexp  12630  mulmoddvds  12632  divalglemeuneg  12692  gcdaddm  12763  dvdsgcdb  12792  mulgcd  12795  gcddiv  12798  uzwodc  12816  lcmdvdsb  12864  mulgcddvds  12874  qredeq  12876  divgcdcoprm0  12881  cncongr1  12883  euclemma  12926  rpexp  12933  rpexp12i  12935  fermltl  13014  prmdiv  13015  odzcllem  13023  odzdvds  13026  odzphi  13027  vfermltl  13032  coprimeprodsq  13038  pythagtriplem6  13051  pythagtriplem7  13052  pythagtriplem12  13056  pythagtriplem13  13057  pceu  13076  pcdvdsb  13101  pcgcd1  13109  dvdsprmpweq  13116  sumhashdc  13128  ctinf  13323  fvsetsid  13388  ressressg  13431  ressabsg  13432  rngplusgg  13493  imasaddvallemg  13638  qusaddvallemg  13656  plusfvalg  13685  mgmb1mgm1  13690  issubmnd  13757  ress0g  13758  imasmnd2  13761  imasmnd  13762  grpasscan2  13871  grpidrcan  13872  grpidlcan  13873  grpinvadd  13885  grpsubeq0  13893  grppncan  13898  dfgrp3mlem  13905  dfgrp3me  13907  grpsubpropd2  13912  imasgrp2  13915  imasgrp  13916  mhmmnd  13921  mulgnn0p1  13938  mulgnnsubcl  13939  mulgnn0subcl  13940  mulgsubcl  13941  mulgneg  13945  mulgaddcom  13951  mulginvcom  13952  submmulg  13971  subgcl  13989  subgsubcl  13990  subgsub  13991  subgmulg  13993  nsgconj  14011  nsgid  14020  quseccl0g  14036  ghmmulg  14061  ghmeqker  14076  f1ghm0to0  14077  kerf1ghm  14079  ablinvadd  14116  ablsub4  14119  ablpncan2  14122  subgabl  14138  gzsumconst  14145  gsumsncmn  14158  gsumconstcmn  14168  pwsinvg  14217  rngcl  14245  imasrng  14257  srgcl  14276  ringcl  14319  crngcom  14320  ringidss  14336  ringcom  14338  imasring  14371  opprringbg  14387  unitmulcl  14422  unitmulclb  14423  dvrcl  14444  unitdvcl  14445  dvrcan1  14449  dvrcan3  14450  rhmmul  14473  subrngrng  14512  subrngmcl  14519  subrgmcl  14543  subrgdv  14548  rrgeq0  14575  domneq0  14583  islmod  14629  scafvalg  14646  lmodcom  14672  rmodislmodlem  14689  rmodislmod  14690  lssclg  14703  lssvnegcl  14715  lssintclm  14723  lspss  14738  lspun  14741  lspsnvsi  14757  rspssp  14833  rnglidlmmgm  14835  rnglidlmsgrp  14836  rnglidlrng  14837  zndvds  14986  aspss  15021  asclmul1  15031  asclmul2  15032  ascldimul  15033  asclinvg  15034  asclmulg  15046  psrbaglecl  15062  psrbagcon  15064  2basgeng  15185  iuncld  15218  ntrss  15222  restco  15277  restabs  15278  cnprcl2k  15309  lmconst  15319  cnrest2  15339  cnmpt2t  15396  psmetsym  15432  psmetge0  15434  xmetge0  15468  xmetsym  15471  blvalps  15491  blval  15492  xblcntrps  15516  xblcntr  15517  xmssym  15572  blsscls2  15596  bdxmet  15604  txmetcnp  15621  dvfvalap  15784  dvid  15798  dvidre  15800  dvcnp2cntop  15802  elplyr  15843  logfac  16001  rpcxpadd  16013  rpcxpsub  16016  rpmulcxp  16017  rpdivcxp  16019  cxpmul  16020  rpcxple2  16026  rpcxplt2  16027  rplogbval  16053  rplogbcl  16054  rplogbreexp  16061  relogbexpap  16066  logbleb  16069  logblt  16070  rplogbcxp  16071  rpcxplogb  16072  relogbcxpbap  16073  sgmppw  16112  bcmono  16124  lgsneg1  16156  lgsmod  16157  lgsne0  16169  lgssq  16171  lgsdirnn0  16178  lgsdinn0  16179  lgsquad  16211  funvtxvalg  16289  funiedgvalg  16290  lpvtx  16332  ausgrumgrien  16423  ausgrusgrien  16424  uhgrissubgr  16514  egrsubgr  16516  subumgredg2en  16524  subusgr  16528  wlkl1loop  16611  clwwlknonex2  16692  eulerpathprum  16733  eulerpathum  16734  findset  16983  repiecele0  17087  repiecege0  17088