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  4541  tfisi  4736  sotri2  5188  sotri3  5189  feq123  5528  sefvex  5719  fvmptt  5800  fnfvima  5956  cocan1  5996  cocan2  5997  ovexg  6122  ovmpox  6220  ovmpoga  6221  fvmpopr2d  6228  caovimo  6286  suppval1  6483  suppimacnvfn  6490  suppfnss  6501  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfrcllembxssdm  6632  tfrcllembfn  6633  freccllem  6678  frecfcllem  6680  frecsuclem  6682  frecrdg  6684  mapm  6975  domssr  7070  mapxpen  7154  dif1en  7189  diffifi  7204  unsnfidcex  7233  unfidisj  7235  undifdc  7237  resfnfinfinss  7259  funrnfi  7262  fissfi  7269  sbthlemi9  7289  elfir  7313  difinfsn  7447  ctssdc  7460  djuassen  7580  xpdjuen  7581  mulcanenq  7759  ltanqg  7774  mulcanenq0ec  7819  addnnnq0  7823  distrprg  7962  aptipr  8015  addsrpr  8119  mulsrpr  8120  mulasssrg  8132  ltpsrprg  8177  axmulass  8247  axpre-ltadd  8260  subadd2  8538  nppcan  8556  nppcan3  8558  subsub2  8562  subsub4  8567  npncan3  8572  pnpcan  8573  pnncan  8575  subcan  8589  ltadd1  8765  leadd1  8766  leadd2  8767  ltsubadd  8768  ltsubadd2  8769  lesubadd  8770  lesubadd2  8771  ltaddsub  8772  leaddsub  8774  lesub1  8792  lesub2  8793  ltsub1  8794  ltsub2  8795  gt0add  8910  apreap  8924  lemul1  8930  reapmul1lem  8931  reapmul1  8932  reapadd1  8933  remulext1  8936  remulext2  8937  apadd2  8946  mulext2  8950  mulap0r  8952  leltap  8962  ltap  8970  apsub1  8979  recexaplem2  8989  mulcanap  9002  mulcanap2  9003  divvalap  9013  divmulap  9014  divcanap1  9020  diveqap0  9021  divap0b  9022  divrecap  9027  divassap  9029  div23ap  9030  divdirap  9036  divcanap3  9037  div11ap  9039  diveqap1  9044  divmuldivap  9051  divcanap5  9053  redivclap  9070  div2negap  9074  apmul1  9127  apmul2  9128  div2subap  9176  ltdiv1  9207  ledivmul  9216  lemuldiv  9220  lt2msq1  9224  ltdiv23  9231  squeeze0  9243  ofsubeq0  9301  ofnegsub  9302  ind1  9310  zaddcllemneg  9693  zfidc  9733  eluzsub  9968  nn01to3  10033  rpgecl  10100  addlelt  10186  xleadd1  10294  xltadd1  10295  lbioog  10332  ubioc1  10348  ubicc2  10404  icoshftf1o  10410  fzen  10464  nelfzo  10576  ubmelfzo  10635  ssfzo12  10659  ubmelm1fzo  10661  fzosplitprm1  10670  zsupssdc  10690  rebtwn2zlemshrink  10705  qbtwnre  10708  icogelb  10717  flqwordi  10744  flqword2  10745  flltdivnn0lt  10760  modqcl  10784  mulqmod0  10788  modqmulnn  10800  modqabs2  10816  modqmuladdnn0  10826  qnegmod  10827  addmodid  10830  modqm1p1mod0  10833  modifeq2int  10844  modqdi  10850  modqeqmodmin  10852  modfzo0difsn  10853  frec2uzf1od  10864  exp3val  10999  expnegap0  11005  expgt1  11035  exprecap  11038  expmulzap  11043  leexp2a  11050  expubnd  11054  mulbinom2  11114  bernneq2  11120  expnbnd  11122  fihashss  11279  fihashssdif  11281  fimaxq  11292  ccatval2  11388  ccatass  11398  ccatw2s1leng  11428  ccat2s1fvwd  11437  swrdval  11442  swrdnd  11453  pfxfv  11478  pfxpfx  11502  ccats1pfxeq  11508  ccats1pfxeqrex  11509  s3cl  11580  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  shftuz  11604  shftfibg  11607  cjdivap  11697  resqrtcl  11817  absdivap  11858  abssubne0  11880  maxleast  12002  lemininf  12024  ltmininf  12025  xrmaxltsup  12049  xrmaxaddlem  12051  xrmaxadd  12052  xrmineqinf  12060  xrltmininf  12061  xrminltinf  12063  xrminadd  12066  climuni  12084  reccn2ap  12104  isumz  12181  geoisum1c  12312  prod1dc  12378  efltim  12490  dvdsval2  12582  dvdscmulr  12612  dvdsmulcr  12613  modmulconst  12615  dvdsadd2b  12632  dvdsexp  12653  mulmoddvds  12655  divalglemeuneg  12715  gcdaddm  12786  dvdsgcdb  12815  mulgcd  12818  gcddiv  12821  uzwodc  12839  lcmdvdsb  12887  mulgcddvds  12897  qredeq  12899  divgcdcoprm0  12904  cncongr1  12906  euclemma  12950  rpexp  12957  rpexp12i  12959  fermltl  13041  prmdiv  13042  odzcllem  13050  odzdvds  13053  odzphi  13054  vfermltl  13059  coprimeprodsq  13065  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem13  13084  pceu  13103  pcdvdsb  13128  pcgcd1  13136  dvdsprmpweq  13143  sumhashdc  13155  ctinf  13379  fvsetsid  13444  ressressg  13488  ressabsg  13489  rngplusgg  13550  imasaddvallemg  13695  qusaddvallemg  13713  plusfvalg  13742  mgmb1mgm1  13747  issubmnd  13814  ress0g  13815  imasmnd2  13818  imasmnd  13819  grpasscan2  13928  grpidrcan  13929  grpidlcan  13930  grpinvadd  13942  grpsubeq0  13950  grppncan  13955  dfgrp3mlem  13962  dfgrp3me  13964  grpsubpropd2  13969  imasgrp2  13972  imasgrp  13973  mhmmnd  13978  mulgnn0p1  13995  mulgnnsubcl  13996  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgaddcom  14008  mulginvcom  14009  submmulg  14028  subgcl  14046  subgsubcl  14047  subgsub  14048  subgmulg  14050  nsgconj  14068  nsgid  14077  quseccl0g  14093  ghmmulg  14118  ghmeqker  14133  f1ghm0to0  14134  kerf1ghm  14136  ablinvadd  14204  ablsub4  14207  ablpncan2  14210  subgabl  14226  gzsumconst  14233  gsumsncmn  14246  gsumconstcmn  14266  pwsinvg  14322  rngcl  14350  imasrng  14362  srgcl  14381  ringcl  14424  crngcom  14425  ringidss  14441  ringcom  14443  imasring  14478  opprringbg  14494  unitmulcl  14529  unitmulclb  14530  dvrcl  14551  unitdvcl  14552  dvrcan1  14556  dvrcan3  14557  rhmmul  14580  subrngrng  14619  subrngmcl  14626  subrgmcl  14650  subrgdv  14655  rrgeq0  14682  domneq0  14690  islmod  14736  scafvalg  14753  lmodcom  14779  rmodislmodlem  14796  rmodislmod  14797  lssclg  14810  lssvnegcl  14822  lssintclm  14830  lspss  14845  lspun  14848  lspsnvsi  14864  rspssp  14940  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  zndvds  15093  aspss  15128  asclmul1  15138  asclmul2  15139  ascldimul  15140  asclinvg  15141  asclmulg  15153  psrbagdceq  15168  psrbaglecl  15173  psrbagcon  15174  psrbagfsuppub  15192  psrringfi  15224  2basgeng  15341  iuncld  15374  ntrss  15378  restco  15433  restabs  15434  cnprcl2k  15465  lmconst  15475  cnrest2  15495  cnmpt2t  15552  psmetsym  15588  psmetge0  15590  xmetge0  15624  xmetsym  15627  blvalps  15647  blval  15648  xblcntrps  15672  xblcntr  15673  xmssym  15728  blsscls2  15752  bdxmet  15760  txmetcnp  15777  dvfvalap  15940  dvid  15954  dvidre  15956  dvcnp2cntop  15958  elplyr  15999  logfac  16159  rpcxpadd  16171  rpcxpsub  16174  rpmulcxp  16175  rpdivcxp  16177  cxpmul  16178  rpcxple2  16186  rpcxplt2  16187  rplogbval  16214  rplogbcl  16215  rplogbreexp  16222  relogbexpap  16227  logbleb  16230  logblt  16231  rplogbcxp  16232  rpcxplogb  16233  relogbcxpbap  16234  sgmppw  16319  bcmono  16337  prmefexple  16341  lgsneg1  16382  lgsmod  16383  lgsne0  16395  lgssq  16397  lgsdirnn0  16404  lgsdinn0  16405  lgsquad  16437  funvtxvalg  16515  funiedgvalg  16516  lpvtx  16558  ausgrumgrien  16649  ausgrusgrien  16650  uhgrissubgr  16740  egrsubgr  16742  subumgredg2en  16750  subusgr  16754  wlkl1loop  16837  clwwlknonex2  16918  eulerpathprum  16959  eulerpathum  16960  findset  17209  repiecele0  17314  repiecege0  17315