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  7441  ctssdc  7454  djuassen  7574  xpdjuen  7575  mulcanenq  7753  ltanqg  7768  mulcanenq0ec  7813  addnnnq0  7817  distrprg  7956  aptipr  8009  addsrpr  8113  mulsrpr  8114  mulasssrg  8126  ltpsrprg  8171  axmulass  8241  axpre-ltadd  8254  subadd2  8532  nppcan  8550  nppcan3  8552  subsub2  8556  subsub4  8561  npncan3  8566  pnpcan  8567  pnncan  8569  subcan  8583  ltadd1  8759  leadd1  8760  leadd2  8761  ltsubadd  8762  ltsubadd2  8763  lesubadd  8764  lesubadd2  8765  ltaddsub  8766  leaddsub  8768  lesub1  8786  lesub2  8787  ltsub1  8788  ltsub2  8789  gt0add  8904  apreap  8918  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  remulext1  8930  remulext2  8931  apadd2  8940  mulext2  8944  mulap0r  8946  leltap  8956  ltap  8964  apsub1  8973  recexaplem2  8983  mulcanap  8996  mulcanap2  8997  divvalap  9007  divmulap  9008  divcanap1  9014  diveqap0  9015  divap0b  9016  divrecap  9021  divassap  9023  div23ap  9024  divdirap  9030  divcanap3  9031  div11ap  9033  diveqap1  9038  divmuldivap  9045  divcanap5  9047  redivclap  9064  div2negap  9068  apmul1  9121  apmul2  9122  div2subap  9170  ltdiv1  9201  ledivmul  9210  lemuldiv  9214  lt2msq1  9218  ltdiv23  9225  squeeze0  9237  ofnegsub  9295  ind1  9303  zaddcllemneg  9688  zfidc  9728  eluzsub  9962  nn01to3  10027  rpgecl  10094  addlelt  10180  xleadd1  10288  xltadd1  10289  lbioog  10326  ubioc1  10342  ubicc2  10398  icoshftf1o  10404  fzen  10458  nelfzo  10570  ubmelfzo  10629  ssfzo12  10653  ubmelm1fzo  10655  fzosplitprm1  10664  zsupssdc  10684  rebtwn2zlemshrink  10699  qbtwnre  10702  icogelb  10711  flqwordi  10737  flqword2  10738  flltdivnn0lt  10753  modqcl  10777  mulqmod0  10781  modqmulnn  10793  modqabs2  10809  modqmuladdnn0  10819  qnegmod  10820  addmodid  10823  modqm1p1mod0  10826  modifeq2int  10837  modqdi  10843  modqeqmodmin  10845  modfzo0difsn  10846  frec2uzf1od  10857  exp3val  10992  expnegap0  10998  expgt1  11028  exprecap  11031  expmulzap  11036  leexp2a  11043  expubnd  11047  mulbinom2  11107  bernneq2  11113  expnbnd  11115  fihashss  11272  fihashssdif  11274  fimaxq  11285  ccatval2  11381  ccatass  11391  ccatw2s1leng  11421  ccat2s1fvwd  11430  swrdval  11435  swrdnd  11446  pfxfv  11471  pfxpfx  11495  ccats1pfxeq  11501  ccats1pfxeqrex  11502  s3cl  11573  s3fv0g  11578  s3fv1g  11579  s3fv2g  11580  shftuz  11597  shftfibg  11600  cjdivap  11690  resqrtcl  11810  absdivap  11851  abssubne0  11873  maxleast  11995  lemininf  12017  ltmininf  12018  xrmaxltsup  12042  xrmaxaddlem  12044  xrmaxadd  12045  xrmineqinf  12053  xrltmininf  12054  xrminltinf  12056  xrminadd  12059  climuni  12077  reccn2ap  12097  isumz  12174  geoisum1c  12305  prod1dc  12371  efltim  12483  dvdsval2  12575  dvdscmulr  12605  dvdsmulcr  12606  modmulconst  12608  dvdsadd2b  12625  dvdsexp  12646  mulmoddvds  12648  divalglemeuneg  12708  gcdaddm  12779  dvdsgcdb  12808  mulgcd  12811  gcddiv  12814  uzwodc  12832  lcmdvdsb  12880  mulgcddvds  12890  qredeq  12892  divgcdcoprm0  12897  cncongr1  12899  euclemma  12943  rpexp  12950  rpexp12i  12952  fermltl  13034  prmdiv  13035  odzcllem  13043  odzdvds  13046  odzphi  13047  vfermltl  13052  coprimeprodsq  13058  pythagtriplem6  13071  pythagtriplem7  13072  pythagtriplem12  13076  pythagtriplem13  13077  pceu  13096  pcdvdsb  13121  pcgcd1  13129  dvdsprmpweq  13136  sumhashdc  13148  ctinf  13372  fvsetsid  13437  ressressg  13480  ressabsg  13481  rngplusgg  13542  imasaddvallemg  13687  qusaddvallemg  13705  plusfvalg  13734  mgmb1mgm1  13739  issubmnd  13806  ress0g  13807  imasmnd2  13810  imasmnd  13811  grpasscan2  13920  grpidrcan  13921  grpidlcan  13922  grpinvadd  13934  grpsubeq0  13942  grppncan  13947  dfgrp3mlem  13954  dfgrp3me  13956  grpsubpropd2  13961  imasgrp2  13964  imasgrp  13965  mhmmnd  13970  mulgnn0p1  13987  mulgnnsubcl  13988  mulgnn0subcl  13989  mulgsubcl  13990  mulgneg  13994  mulgaddcom  14000  mulginvcom  14001  submmulg  14020  subgcl  14038  subgsubcl  14039  subgsub  14040  subgmulg  14042  nsgconj  14060  nsgid  14069  quseccl0g  14085  ghmmulg  14110  ghmeqker  14125  f1ghm0to0  14126  kerf1ghm  14128  ablinvadd  14165  ablsub4  14168  ablpncan2  14171  subgabl  14187  gzsumconst  14194  gsumsncmn  14207  gsumconstcmn  14217  pwsinvg  14266  rngcl  14294  imasrng  14306  srgcl  14325  ringcl  14368  crngcom  14369  ringidss  14385  ringcom  14387  imasring  14420  opprringbg  14436  unitmulcl  14471  unitmulclb  14472  dvrcl  14493  unitdvcl  14494  dvrcan1  14498  dvrcan3  14499  rhmmul  14522  subrngrng  14561  subrngmcl  14568  subrgmcl  14592  subrgdv  14597  rrgeq0  14624  domneq0  14632  islmod  14678  scafvalg  14695  lmodcom  14721  rmodislmodlem  14738  rmodislmod  14739  lssclg  14752  lssvnegcl  14764  lssintclm  14772  lspss  14787  lspun  14790  lspsnvsi  14806  rspssp  14882  rnglidlmmgm  14884  rnglidlmsgrp  14885  rnglidlrng  14886  zndvds  15035  aspss  15070  asclmul1  15080  asclmul2  15081  ascldimul  15082  asclinvg  15083  asclmulg  15095  psrbaglecl  15111  psrbagcon  15113  2basgeng  15235  iuncld  15268  ntrss  15272  restco  15327  restabs  15328  cnprcl2k  15359  lmconst  15369  cnrest2  15389  cnmpt2t  15446  psmetsym  15482  psmetge0  15484  xmetge0  15518  xmetsym  15521  blvalps  15541  blval  15542  xblcntrps  15566  xblcntr  15567  xmssym  15622  blsscls2  15646  bdxmet  15654  txmetcnp  15671  dvfvalap  15834  dvid  15848  dvidre  15850  dvcnp2cntop  15852  elplyr  15893  logfac  16051  rpcxpadd  16063  rpcxpsub  16066  rpmulcxp  16067  rpdivcxp  16069  cxpmul  16070  rpcxple2  16076  rpcxplt2  16077  rplogbval  16103  rplogbcl  16104  rplogbreexp  16111  relogbexpap  16116  logbleb  16119  logblt  16120  rplogbcxp  16121  rpcxplogb  16122  relogbcxpbap  16123  sgmppw  16208  bcmono  16226  prmefexple  16230  lgsneg1  16266  lgsmod  16267  lgsne0  16279  lgssq  16281  lgsdirnn0  16288  lgsdinn0  16289  lgsquad  16321  funvtxvalg  16399  funiedgvalg  16400  lpvtx  16442  ausgrumgrien  16533  ausgrusgrien  16534  uhgrissubgr  16624  egrsubgr  16626  subumgredg2en  16634  subusgr  16638  wlkl1loop  16721  clwwlknonex2  16802  eulerpathprum  16843  eulerpathum  16844  findset  17093  repiecele0  17197  repiecege0  17198