Theorem simpl2 1194

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl2	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Proof of Theorem simpl2

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1188	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpl12  1251  simpl22  1254  simpl32  1257  simp1l2  1269  simp2l2  1275  simp3l2  1281  3anandirs  1475  rspc3ev  3594  2nreu  4397  f1prex  7232  weniso  7302  ofmpteq  7647  tfisi  7803  mposn  8047  fprlem1  8244  smogt  8301  smocdmdom  8302  omeulem1  8511  nnmord  8562  nnmword  8563  naddasslem1  8624  naddasslem2  8625  difsnen  8991  enfixsn  9018  mapunen  9078  ac6sfi  9188  ordiso2  9424  wemaplem2  9456  wemapso2lem  9461  en2eqpr  9921  acndom  9965  infmap2  10131  cflim2  10177  cfsmolem  10184  coftr  10187  fin23lem26  10239  isf32lem9  10275  fin1a2lem9  10322  fin1a2lem10  10323  gchdomtri  10544  canth4  10562  gchpwdom  10585  gruima  10717  grudomon  10732  prn0  10904  distrlem4pr  10941  prlem934  10948  addcan  11321  addcan2  11322  divmulass  11823  divmulasscom  11824  ltmul1a  11994  supmul1  12115  uzsupss  12857  xaddass  13168  xleadd1a  13172  xlesubadd  13182  xmulass  13206  xlemul2a  13208  xadddilem  13213  xadddi  13214  ixxdisj  13280  ixxun  13281  ixxlb  13287  icoshftf1o  13394  icodisj  13396  ioounsn  13397  lincmb01cmp  13415  iccf1o  13416  elfz1b  13513  ssfzoulel  13680  fzoopth  13682  modmuladd  13840  modaddmulmod  13865  ltexp2a  14093  leexp2  14098  ltexp2r  14100  exple1  14104  expnlbnd2  14161  mulsubdivbinom2  14189  fun2dmnop0  14431  ccatass  14516  ccatopth  14643  pfxccatin12lem2a  14654  repswpfx  14712  repswccat  14713  cshwidxmodr  14731  2cshw  14740  repsco  14767  s2f1o  14843  limsupgle  15404  limsupgre  15408  addcn2  15521  mulcn2  15523  binomrisefac  15969  dvdsval2  16186  dvdsadd2b  16237  dvdsmod  16260  oexpneg  16276  sadass  16402  gcdass  16478  rplpwr  16489  lcmass  16545  coprmdvds2  16585  rpmulgcd2  16587  rpdvds  16591  coprmprod  16592  cncongr2  16599  rpexp  16653  prmdiveq  16717  hashgcdlem  16719  odzdvds  16727  coprimeprodsq2  16741  pythagtriplem3  16750  pythagtriplem4  16751  pcdvdsb  16801  vdwnnlem1  16927  0ram  16952  ramz2  16956  ramub1lem1  16958  mremre  17527  mrieqv2d  17566  lubss  18440  lubun  18442  clatleglb  18445  clatglbss  18446  mrelatglb  18487  isnsgrp  18652  issubmnd  18690  gsumccat  18770  frmdss2  18792  submefmnd  18824  nmzsubg  19098  ghmnsgima  19173  gsmsymgreqlem1  19363  psgnunilem4  19430  odmodnn0  19473  odnncl  19478  odmod  19479  oddvds  19480  odeq  19483  odmulgid  19487  odmulgeq  19490  odbezout  19491  odf1o1  19505  odf1o2  19506  odngen  19510  gexdvdsi  19516  pgpfi1  19528  odcau  19537  subgslw  19549  fislw  19558  lsmless1x  19577  lsmless2x  19578  lsmsubm  19586  lsmmod  19608  lsmmod2  19609  efgsfo  19672  odadd1  19781  odadd2  19782  odadd  19783  lsmcomx  19789  prdscmnd  19794  gsumconst  19867  ablsimpgfindlem1  20042  srg1zr  20154  csrgbinom  20171  ring1eq0  20237  mulgass2  20248  rngisom1  20406  rhmdvdsr  20445  cntzsubrng  20504  cntzsubr  20543  isabvd  20749  rmodislmod  20885  0lmhm  20996  lmhmvsca  21001  reslmhm2b  21010  pwssplit1  21015  pwssplit2  21016  pwssplit3  21017  lbspss  21038  lspsnat  21104  lidldvgen  21293  xrsdsreclblem  21371  cssmre  21652  obs2ss  21688  uvcresum  21752  frlmsslsp  21755  frlmup4  21760  lindff1  21779  f1lindf  21781  lsslindf  21789  islindf4  21797  issubassa  21826  evlsval2  22046  coe1subfv  22212  coe1sclmul  22228  coe1sclmul2  22230  mpomatmul  22394  mamutpos  22406  scmatscmide  22455  mavmulsolcl  22499  mulmarep1gsum2  22522  mdetdiaglem  22546  mdetdiag  22547  mdetunilem1  22560  mdetunilem3  22562  mdetunilem9  22568  maducoeval2  22588  madurid  22592  slesolinvbi  22629  cramerimplem1  22631  cramerlem1  22635  cramer  22639  cpmatel2  22661  m2cpm  22689  m2pmfzmap  22695  m2cpminvid2lem  22702  m2cpminvid2  22703  decpmatmul  22720  pmatcollpw1lem2  22723  pmatcollpw1  22724  pmatcollpw2lem  22725  pmatcollpwfi  22730  pm2mpcl  22745  mply1topmatcl  22753  mp2pm2mplem2  22755  mp2pm2mplem4  22757  mp2pm2mplem5  22758  mp2pm2mp  22759  pm2mpghmlem2  22760  pm2mpghmlem1  22761  chfacfisfcpmat  22803  topssnei  23072  cnconst2  23231  cnpresti  23236  cnprest2  23238  cnpdis  23241  cnt0  23294  cnt1  23298  cnhaus  23302  sscmp  23353  hauscmp  23355  cnconn  23370  unconn  23377  finlocfin  23468  comppfsc  23480  kgen2ss  23503  ptpjopn  23560  prdstopn  23576  ptrescn  23587  qtopss  23663  kqfvima  23678  fbssint  23786  fbasrn  23832  filuni  23833  fmss  23894  rnelfm  23901  fmufil  23907  fmco  23909  flimss2  23920  flimss1  23921  flimrest  23931  cnpflf2  23948  flfcnp  23952  supnfcls  23968  fclsss1  23970  fclsss2  23971  isfcf  23982  subgntr  24055  opnsubg  24056  cldsubg  24059  ghmcnp  24063  ustuqtop1  24189  bldisj  24346  blgt0  24347  bl2in  24348  blss2ps  24351  blss2  24352  blssps  24372  blss  24373  xmetresbl  24385  lpbl  24451  blcld  24453  stdbdmopn  24466  metcnp3  24488  metcnp  24489  metcnp2  24490  txmetcnp  24495  blval2  24510  nmoix  24677  nmoi2  24678  nmotri  24687  metdsge  24798  metdseq0  24803  iocopnst  24897  xrhmeo  24904  nmhmcn  25080  cphsqrtcl2  25146  cphsqrtcl3  25147  cssbn  25335  pjth  25399  ovoliunlem2  25464  volun  25506  mbfimaopn2  25618  iblconst  25779  limcvallem  25832  dvfval  25858  dvcnp2  25881  dvcnp2OLD  25882  dvcn  25883  deg1mul3le  26082  deg1tmle  26083  dvdsq1p  26128  idomrootle  26138  ig1peu  26140  ig1pdvds  26145  ply1term  26169  coeid3  26205  dgrmulc  26237  dvply1  26251  aaliou2  26308  efcvx  26419  tanord  26507  eflogeq  26571  logdivlti  26589  logccv  26632  recxpcl  26644  cxplea  26665  cxpeq  26727  ang180  26784  isosctrlem2  26789  cxp2lim  26947  amgm  26961  muval1  27103  dvdssqf  27108  mumullem2  27150  mumul  27151  bcmono  27248  lgsneg  27292  lgsdilem  27295  lgsdirprm  27302  lgsdir  27303  lgsdi  27305  lgsne0  27306  nolesgn2o  27643  nogesgn1o  27645  nosep1o  27653  nosep2o  27654  nosepssdm  27658  nosupres  27679  nosupbnd1lem1  27680  nosupbnd1lem4  27683  nosupbnd1lem5  27684  nosupbnd1lem6  27685  noinfres  27694  noinfbnd1lem1  27695  noinfbnd1lem4  27698  noinfbnd1lem6  27700  noinfbnd2  27703  noetasuplem3  27707  noetainflem3  27711  slelss  27891  cofsslt  27900  coinitsslt  27901  cofcutrtime  27909  addsass  27987  addsdi  28137  mulsass  28148  sltmul2  28153  divsmulw  28175  bdayfinbndlem1  28446  zs12bdaylem  28463  brbtwn2  28961  colinearalglem1  28962  colinearalg  28966  axcgrtr  28971  axsegconlem8  28980  axsegconlem9  28981  axsegconlem10  28982  axcontlem2  29021  axcontlem10  29029  elntg2  29041  ewlkle  29662  crctcshwlkn0lem5  29870  wwlknp  29899  wwlksnext  29949  wwlksnextproplem1  29965  wspthsnwspthsnon  29972  clwlkclwwlklem3  30059  erclwwlksym  30079  erclwwlknsym  30128  upgriseupth  30265  eucrct2eupth  30303  3cyclfrgrrn  30344  numclwwlk2lem1lem  30400  numclwwlk1lem2foa  30412  frgrregord13  30454  nvmul0or  30708  ipval2lem2  30762  lnoadd  30816  lnosub  30817  lnomul  30818  shless  31417  shlej1  31418  kbmul  32013  homco2  32035  kbass2  32175  eliccelico  32838  elicoelioo  32839  iocinioc2  32840  iocinif  32842  difioo  32843  nexple  32906  swrdrn2  33017  swrdrn3  33018  xrge0adddir  33081  xrge0npcan  33083  isarchi2  33248  archiabl  33261  pidlnz  33438  lindssn  33440  ssmxidl  33536  pstmfval  34034  fmcncfil  34069  zrhnm  34105  qqhnm  34128  volfiniune  34368  dya2iocnrect  34419  probinc  34559  cndprob01  34573  signswmnd  34695  bnj517  35022  cvmsss2  35449  cvmlift2lem10  35487  br6  35932  funsseq  35943  cgrtriv  36177  5segofs  36181  btwnouttr2  36197  btwnxfr  36231  lineext  36251  btwnconn1lem13  36274  brsegle2  36284  nn0prpwlem  36497  weiunpo  36640  weiunso  36641  weiunfr  36642  weiunse  36643  lindsenlbs  37787  blbnd  37959  ismtyima  37975  rrndstprj2  38003  ghomdiv  38064  grpokerinj  38065  lsatfixedN  39306  lssat  39313  lshpkrlem4  39410  cvrcon3b  39574  atlen0  39607  atcvreq0  39611  atnle  39614  atlatmstc  39616  atlatle  39617  cvlcvr1  39636  hlsupr2  39684  hlrelat2  39700  cvrexchlem  39716  lnnat  39724  atcvrj2b  39729  3dimlem3  39758  3dim1  39764  1cvrjat  39772  llni  39805  llni2  39809  llnexatN  39818  2llnmat  39821  lplni  39829  2atnelpln  39841  llncvrlpln2  39854  2llnmj  39857  lplnexatN  39860  lplnexllnN  39861  2llnm3N  39866  lvoli  39872  lvoli3  39874  lvolnle3at  39879  islvol2aN  39889  4atlem4a  39896  4atlem4b  39897  4atlem11  39906  lplncvrlvol2  39912  2lplnmj  39919  islinei  40037  linepmap  40072  lnjatN  40077  lncvrat  40079  lncmp  40080  elpaddn0  40097  elpaddatriN  40100  elpaddat  40101  paddcom  40110  paddss2  40115  paddss12  40116  paddasslem4  40120  paddasslem9  40125  paddasslem10  40126  pmodl42N  40148  pmapjoin  40149  llnmod1i2  40157  polcon2bN  40217  pclfinclN  40247  poml4N  40250  poml6N  40252  osumcllem1N  40253  osumcllem2N  40254  osumcllem11N  40263  osumclN  40264  pmapojoinN  40265  pexmidlem2N  40268  pexmidlem3N  40269  pexmidlem4N  40270  pexmidlem6N  40272  pexmidlem7N  40273  pl42lem2N  40277  pl42lem3N  40278  pl42lem4N  40279  pl42N  40280  lhprelat3N  40337  4atex  40373  lauteq  40392  lautco  40394  ltrncoidN  40425  ltrneq2  40445  ltrnideq  40472  trlnle  40483  trlval3  40484  cdlemc  40494  cdlemd9  40503  cdlemd  40504  cdleme21j  40633  cdleme21  40634  cdleme29ex  40671  cdlemefr27cl  40700  cdlemefs27cl  40710  cdleme32d  40741  cdleme32f  40743  cdleme35h2  40754  cdleme40m  40764  cdleme17d3  40793  cdleme48fvg  40797  cdlemeg46fvcl  40803  cdlemeg46fgN  40831  cdleme48fgv  40835  cdleme50trn3  40850  cdlemb3  40903  cdlemg8  40928  cdlemg11a  40934  cdlemg15a  40952  cdlemg15  40953  cdlemg16  40954  cdlemg16z  40956  cdlemg17dN  40960  cdlemg24  40985  cdlemg37  40986  cdlemg29  41002  cdlemg33b  41004  cdlemg38  41012  cdlemg40  41014  trlco  41024  cdlemg44b  41029  ltrncom  41035  trljco  41037  tendococl  41069  tendoplcl  41078  tendoplcom  41079  cdlemj2  41119  tendoid0  41122  tendo1ne0  41125  cdlemk25-3  41201  cdlemk36  41210  cdlemkid4  41231  cdlemk19x  41240  cdlemk53  41254  cdlemk56  41268  cdleml5N  41277  tendospcanN  41320  cdlemm10N  41415  dihord6apre  41553  dihord  41561  dihmeetlem1N  41587  dihglblem2N  41591  dihmeetlem2N  41596  dihmeetbN  41600  dihmeetlem5  41605  dihmeetlem6  41606  dihmeetlem7N  41607  dihmeetlem10N  41613  dihmeetlem12N  41615  dihmeetlem16N  41619  dihmeetlem17N  41620  dihmeetlem18N  41621  dihmeetALTN  41624  dihlspsnssN  41629  dvh3dim2  41745  dvh3dim3N  41746  lcfrlem16  41855  mapdrvallem2  41942  mapdh8ad  42076  hgmapvvlem3  42222  sticksstones1  42437  sticksstones2  42438  aks6d1c6isolem1  42465  resubcan2  42679  diophrw  43037  eldioph2lem1  43038  diophrex  43053  rencldnfi  43099  pellexlem2  43108  pellqrexplicit  43155  infmrgelbi  43156  pellfundglb  43163  pellfund14gap  43165  rmxycomplete  43195  congadd  43244  acongeq  43261  jm2.19  43271  jm2.23  43274  jm2.20nn  43275  jm2.27  43286  jm3.1  43298  lnmepi  43363  lmhmlnmsplit  43365  hbtlem2  43402  dgraa0p  43427  proot1hash  43473  iocunico  43489  iocinico  43490  oasubex  43564  cantnf2  43603  onmcl  43609  omcl2  43611  nadd2rabex  43664  nadd1rabtr  43666  nadd1rabex  43668  fzunt  43732  relexpxpmin  43994  ntrclsk3  44347  grur1cld  44509  ismnu  44538  grumnudlem  44562  ismnushort  44578  rfcnnnub  45317  uzwo4  45334  wessf1ornlem  45465  supxrge  45619  infleinflem2  45651  iccintsng  45805  climsuse  45890  lptre2pt  45920  limcleqr  45924  0ellimcdiv  45929  fnlimfvre  45954  dvnprodlem1  46226  volioc  46252  stoweidlem17  46297  stoweidlem19  46299  stoweidlem20  46300  stoweidlem22  46302  stoweidlem28  46308  stoweidlem34  46314  stoweidlem44  46324  stoweidlem60  46340  wallispilem3  46347  fourierdlem42  46429  fourierdlem48  46434  fourierdlem51  46437  fourierdlem54  46440  fourierdlem74  46460  fourierdlem77  46463  fourierdlem87  46473  fourierdlem97  46483  ioorrnopnlem  46584  ovnsubaddlem2  46851  smfinflem  47097  fsupdm  47122  finfdm  47126  eluzge0nn0  47594  fzopredsuc  47605  imasetpreimafvbijlemfv  47684  lighneallem4  47892  oexpnegALTV  47959  oexpnegnz  47960  tgblthelfgott  48097  clnbgrgrim  48216  isubgr3stgrlem3  48250  rmsupp0  48650  rmsuppss  48652  lincresunit3lem3  48756  lincresunit3lem2  48762  lindssnlvec  48768  fdivmptf  48823  refdivmptf  48824  elbigolo1  48839  rrx2linest  49024  itsclc0lem1  49038  itsclc0lem2  49039  itsclc0yqsollem1  49044  itsclc0b  49054  setc1onsubc  49883