Theorem simpl2 1210

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 487	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2	1	3ad2antl2 1204	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  simpl12  1267  simpl22  1270  simpl32  1273  simp1l2  1285  simp2l2  1291  simp3l2  1297  3anandirs  1500  rspc3ev  3597  2nreu  4408  f1prex  7282  weniso  7354  ofmpteq  7699  tfisi  7853  mposn  8096  fprlem1  8295  smogt  8352  smocdmdom  8353  omeulem1  8565  nnmord  8616  nnmword  8617  naddasslem1  8679  naddasslem2  8680  difsnen  9045  enfixsn  9072  mapunen  9132  ac6sfi  9242  ordiso2  9475  wemaplem2  9507  wemapso2lem  9512  en2eqpr  9998  acndom  10042  infmap2  10207  cflim2  10253  cfsmolem  10260  coftr  10263  fin23lem26  10315  isf32lem9  10351  fin1a2lem9  10398  fin1a2lem10  10399  gchdomtri  10620  canth4  10638  gchpwdom  10661  gruima  10793  grudomon  10808  prn0  10980  distrlem4pr  11017  prlem934  11024  addcan  11400  addcan2  11401  divmulass  11901  divmulasscom  11902  ltmul1a  12070  supmul1  12190  uzsupss  12970  xaddass  13281  xleadd1a  13285  xlesubadd  13295  xmulass  13319  xlemul2a  13321  xadddilem  13326  xadddi  13327  ixxdisj  13393  ixxun  13394  ixxlb  13400  icoshftf1o  13507  icodisj  13509  ioounsn  13510  lincmb01cmp  13528  iccf1o  13529  elfz1b  13628  ssfzoulel  13796  fzoopth  13798  modmuladd  13956  modaddmulmod  13981  ltexp2a  14209  leexp2  14214  ltexp2r  14216  exple1  14220  expnlbnd2  14277  mulsubdivbinom2  14305  fun2dmnop0  14548  ccatass  14633  ccatopth  14760  pfxccatin12lem2a  14771  repswpfx  14829  repswccat  14830  cshwidxmodr  14848  2cshw  14857  repsco  14884  s2f1o  14960  limsupgle  15535  limsupgre  15539  addcn2  15652  mulcn2  15654  binomrisefac  16102  dvdsval2  16319  dvdsadd2b  16370  dvdsmod  16393  oexpneg  16409  sadass  16535  gcdass  16611  rplpwr  16622  lcmass  16678  coprmdvds2  16718  rpmulgcd2  16720  rpdvds  16724  coprmprod  16725  cncongr2  16732  rpexp  16787  prmdiveq  16851  hashgcdlem  16853  odzdvds  16861  coprimeprodsq2  16875  pythagtriplem3  16884  pythagtriplem4  16885  pcdvdsb  16935  vdwnnlem1  17061  0ram  17086  ramz2  17090  ramub1lem1  17092  mremre  17662  mrieqv2d  17701  lubss  18575  lubun  18577  clatleglb  18580  clatglbss  18581  mrelatglb  18622  isnsgrp  18787  issubmnd  18825  gsumccat  18906  frmdss2  18928  submefmnd  18960  nmzsubg  19237  ghmnsgima  19316  gsmsymgreqlem1  19506  psgnunilem4  19573  odmodnn0  19616  odnncl  19621  odmod  19622  oddvds  19623  odeq  19626  odmulgid  19630  odmulgeq  19633  odbezout  19634  odf1o1  19648  odf1o2  19649  odngen  19653  gexdvdsi  19659  pgpfi1  19671  odcau  19680  subgslw  19692  fislw  19701  lsmless1x  19720  lsmless2x  19721  lsmsubm  19729  lsmmod  19751  lsmmod2  19752  efgsfo  19815  odadd1  19924  odadd2  19925  odadd  19926  lsmcomx  19932  prdscmnd  19937  gsumconst  20010  ablsimpgfindlem1  20185  csrgbinom  20320  ring1eq0  20388  mulgass2  20399  rngisom1  20555  rhmdvdsr  20616  cntzsubrng  20677  cntzsubr  20716  isdrng3lem2  20863  isabvd  20926  rmodislmod  21062  0lmhm  21172  lmhmvsca  21177  reslmhm2b  21186  pwssplit1  21191  pwssplit2  21192  pwssplit3  21193  lbspss  21214  lspsnat  21280  pidlnz  21385  lidldvgen  21513  xrsdsreclblem  21574  cssmre  21854  obs2ss  21890  uvcresum  21954  frlmsslsp  21957  frlmup4  21962  lindff1  21981  f1lindf  21983  lsslindf  21991  islindf4  21999  issubassa  22028  evlsval2  22249  coe1subfv  22438  coe1sclmul  22454  coe1sclmul2  22456  mpomatmul  22614  mamutpos  22626  scmatscmide  22675  mavmulsolcl  22719  mulmarep1gsum2  22742  mdetdiaglem  22766  mdetdiag  22767  mdetunilem1  22780  mdetunilem3  22782  mdetunilem9  22788  maducoeval2  22808  madurid  22812  slesolinvbi  22849  cramerimplem1  22851  cramerlem1  22855  cramer  22859  cpmatel2  22881  m2cpm  22909  m2pmfzmap  22915  m2cpminvid2lem  22922  m2cpminvid2  22923  decpmatmul  22940  pmatcollpw1lem2  22943  pmatcollpw1  22944  pmatcollpw2lem  22945  pmatcollpwfi  22950  pm2mpcl  22965  mply1topmatcl  22973  mp2pm2mplem2  22975  mp2pm2mplem4  22977  mp2pm2mplem5  22978  mp2pm2mp  22979  pm2mpghmlem2  22980  pm2mpghmlem1  22981  chfacfisfcpmat  23023  topssnei  23292  cnconst2  23451  cnpresti  23456  cnprest2  23458  cnpdis  23461  cnt0  23514  cnt1  23518  cnhaus  23522  sscmp  23573  hauscmp  23575  cnconn  23590  unconn  23597  finlocfin  23688  comppfsc  23700  kgen2ss  23723  ptpjopn  23780  prdstopn  23796  ptrescn  23807  qtopss  23883  kqfvima  23898  fbssint  24006  fbasrn  24052  filuni  24053  fmss  24114  rnelfm  24121  fmufil  24127  fmco  24129  flimss2  24140  flimss1  24141  flimrest  24151  cnpflf2  24168  flfcnp  24172  supnfcls  24188  fclsss1  24190  fclsss2  24191  isfcf  24202  subgntr  24275  opnsubg  24276  cldsubg  24279  ghmcnp  24283  ustuqtop1  24409  bldisj  24566  blgt0  24567  bl2in  24568  blss2ps  24571  blss2  24572  blssps  24592  blss  24593  xmetresbl  24605  lpbl  24671  blcld  24673  stdbdmopn  24686  metcnp3  24708  metcnp  24709  metcnp2  24710  txmetcnp  24715  blval2  24730  nmoix  24897  nmoi2  24898  nmotri  24907  metdsge  25018  metdseq0  25023  iocopnst  25110  xrhmeo  25116  nmhmcn  25290  cphsqrtcl2  25356  cphsqrtcl3  25357  cssbn  25545  pjth  25609  ovoliunlem2  25673  volun  25715  mbfimaopn2  25827  iblconst  25988  limcvallem  26041  dvfval  26067  dvcnp2  26090  dvcn  26091  deg1mul3le  26285  deg1tmle  26286  dvdsq1p  26331  idomrootle  26341  ig1peu  26343  ig1pdvds  26348  ply1term  26372  coeid3  26408  dgrmulc  26439  dvply1  26456  aaliou2  26514  efcvx  26623  tanord  26714  eflogeq  26778  logdivlti  26796  logccv  26839  recxpcl  26851  cxplea  26872  cxpeq  26933  ang180  26990  isosctrlem2  26995  cxp2lim  27152  amgm  27166  muval1  27308  dvdssqf  27313  mumullem2  27355  mumul  27356  bcmono  27452  lgsneg  27496  lgsdilem  27499  lgsdirprm  27506  lgsdir  27507  lgsdi  27509  lgsne0  27510  nolesgn2o  27846  nogesgn1o  27848  nosep1o  27856  nosep2o  27857  nosepssdm  27861  nosupres  27882  nosupbnd1lem1  27883  nosupbnd1lem4  27886  nosupbnd1lem5  27887  nosupbnd1lem6  27888  noinfres  27897  noinfbnd1lem1  27898  noinfbnd1lem4  27901  noinfbnd1lem6  27903  noinfbnd2  27906  noetasuplem3  27910  noetainflem3  27914  leslss  28113  cofslts  28122  coinitslts  28123  cofcutrtime  28131  addsass  28209  addsdi  28359  mulsass  28370  ltmuls2  28375  divmulsw  28397  bdayfinbndlem1  28671  z12bdaylem  28688  brbtwn2  29266  colinearalglem1  29267  colinearalg  29271  axcgrtr  29276  axsegconlem8  29285  axsegconlem9  29286  axsegconlem10  29287  axcontlem2  29326  axcontlem10  29334  elntg2  29346  ewlkle  29966  crctcshwlkn0lem5  30174  wwlknp  30203  wwlksnext  30253  wwlksnextproplem1  30269  wspthsnwspthsnon  30276  clwlkclwwlklem3  30363  erclwwlksym  30383  erclwwlknsym  30432  upgriseupth  30569  eucrct2eupth  30607  3cyclfrgrrn  30648  numclwwlk2lem1lem  30704  numclwwlk1lem2foa  30716  frgrregord13  30758  nvmul0or  31013  ipval2lem2  31067  lnoadd  31121  lnosub  31122  lnomul  31123  shless  31722  shlej1  31723  kbmul  32318  homco2  32340  kbass2  32480  eliccelico  33133  elicoelioo  33134  iocinioc2  33135  iocinif  33137  difioo  33138  nexple  33188  swrdrn2  33283  swrdrn3  33284  xrge0adddir  33347  xrge0npcan  33349  isarchi2  33514  archiabl  33527  lindssn  33700  ssmxidl  33766  pstmfval  34295  fmcncfil  34330  zrhnm  34366  qqhnm  34389  volfiniune  34629  dya2iocnrect  34680  probinc  34820  cndprob01  34834  signswmnd  34953  bnj517  35282  cvmsss2  35774  cvmlift2lem10  35812  br6  36257  funsseq  36268  cgrtriv  36502  5segofs  36506  btwnouttr2  36522  btwnxfr  36556  lineext  36576  btwnconn1lem13  36599  brsegle2  36609  nmulss1  36714  ltnmul  36716  nmulle  36717  ltnadd  36718  naddle  36719  nadddi  36724  nn0prpwlem  36861  weiunpo  37004  weiunso  37005  weiunfr  37006  weiunse  37007  axtcond  37017  lindsenlbs  38294  blbnd  38466  ismtyima  38482  rrndstprj2  38510  ghomdiv  38571  grpokerinj  38572  lsatfixedN  39811  lssat  39818  lshpkrlem4  39915  cvrcon3b  40079  atlen0  40112  atcvreq0  40116  atnle  40119  atlatmstc  40121  atlatle  40122  cvlcvr1  40141  hlsupr2  40189  hlrelat2  40205  cvrexchlem  40221  lnnat  40229  atcvrj2b  40234  3dimlem3  40263  3dim1  40269  1cvrjat  40277  llni  40310  llni2  40314  llnexatN  40323  2llnmat  40326  lplni  40334  2atnelpln  40346  llncvrlpln2  40359  2llnmj  40362  lplnexatN  40365  lplnexllnN  40366  2llnm3N  40371  lvoli  40377  lvoli3  40379  lvolnle3at  40384  islvol2aN  40394  4atlem4a  40401  4atlem4b  40402  4atlem11  40411  lplncvrlvol2  40417  2lplnmj  40424  islinei  40542  linepmap  40577  lnjatN  40582  lncvrat  40584  lncmp  40585  elpaddn0  40602  elpaddatriN  40605  elpaddat  40606  paddcom  40615  paddss2  40620  paddss12  40621  paddasslem4  40625  paddasslem9  40630  paddasslem10  40631  pmodl42N  40653  pmapjoin  40654  llnmod1i2  40662  polcon2bN  40722  pclfinclN  40752  poml4N  40755  poml6N  40757  osumcllem1N  40758  osumcllem2N  40759  osumcllem11N  40768  osumclN  40769  pmapojoinN  40770  pexmidlem2N  40773  pexmidlem3N  40774  pexmidlem4N  40775  pexmidlem6N  40777  pexmidlem7N  40778  pl42lem2N  40782  pl42lem3N  40783  pl42lem4N  40784  pl42N  40785  lhprelat3N  40842  4atex  40878  lauteq  40897  lautco  40899  ltrncoidN  40930  ltrneq2  40950  ltrnideq  40977  trlnle  40988  trlval3  40989  cdlemc  40999  cdlemd9  41008  cdlemd  41009  cdleme21j  41138  cdleme21  41139  cdleme29ex  41176  cdlemefr27cl  41205  cdlemefs27cl  41215  cdleme32d  41246  cdleme32f  41248  cdleme35h2  41259  cdleme40m  41269  cdleme17d3  41298  cdleme48fvg  41302  cdlemeg46fvcl  41308  cdlemeg46fgN  41336  cdleme48fgv  41340  cdleme50trn3  41355  cdlemb3  41408  cdlemg8  41433  cdlemg11a  41439  cdlemg15a  41457  cdlemg15  41458  cdlemg16  41459  cdlemg16z  41461  cdlemg17dN  41465  cdlemg24  41490  cdlemg37  41491  cdlemg29  41507  cdlemg33b  41509  cdlemg38  41517  cdlemg40  41519  trlco  41529  cdlemg44b  41534  ltrncom  41540  trljco  41542  tendococl  41574  tendoplcl  41583  tendoplcom  41584  cdlemj2  41624  tendoid0  41627  tendo1ne0  41630  cdlemk25-3  41706  cdlemk36  41715  cdlemkid4  41736  cdlemk19x  41745  cdlemk53  41759  cdlemk56  41773  cdleml5N  41782  tendospcanN  41825  cdlemm10N  41920  dihord6apre  42058  dihord  42066  dihmeetlem1N  42092  dihglblem2N  42096  dihmeetlem2N  42101  dihmeetbN  42105  dihmeetlem5  42110  dihmeetlem6  42111  dihmeetlem7N  42112  dihmeetlem10N  42118  dihmeetlem12N  42120  dihmeetlem16N  42124  dihmeetlem17N  42125  dihmeetlem18N  42126  dihmeetALTN  42129  dihlspsnssN  42134  dvh3dim2  42250  dvh3dim3N  42251  lcfrlem16  42360  mapdrvallem2  42447  mapdh8ad  42581  hgmapvvlem3  42727  sticksstones1  42941  sticksstones2  42942  aks6d1c6isolem1  42969  resubcan2  43177  diophrw  43518  eldioph2lem1  43519  diophrex  43534  rencldnfi  43576  pellexlem2  43585  pellqrexplicit  43632  infmrgelbi  43633  pellfundglb  43640  pellfund14gap  43642  rmxycomplete  43672  congadd  43721  acongeq  43738  jm2.19  43748  jm2.23  43751  jm2.20nn  43752  jm2.27  43763  jm3.1  43775  lnmepi  43840  lmhmlnmsplit  43842  hbtlem2  43879  dgraa0p  43904  proot1hash  43950  iocunico  43966  iocinico  43967  oasubex  44041  cantnf2  44080  onmcl  44086  omcl2  44088  nadd2rabex  44141  nadd1rabtr  44143  nadd1rabex  44145  fzunt  44209  relexpxpmin  44471  ntrclsk3  44824  grur1cld  44984  ismnu  44999  grumnudlem  45023  ismnushort  45039  rfcnnnub  45784  uzwo4  45801  wessf1ornlem  45931  supxrge  46082  infleinflem2  46114  iccintsng  46267  climsuse  46352  lptre2pt  46382  limcleqr  46386  0ellimcdiv  46391  fnlimfvre  46416  dvnprodlem1  46688  volioc  46714  stoweidlem17  46759  stoweidlem19  46761  stoweidlem20  46762  stoweidlem22  46764  stoweidlem28  46770  stoweidlem34  46776  stoweidlem44  46786  stoweidlem60  46802  wallispilem3  46809  fourierdlem42  46891  fourierdlem48  46896  fourierdlem51  46899  fourierdlem54  46902  fourierdlem74  46922  fourierdlem77  46925  fourierdlem87  46935  fourierdlem97  46945  ioorrnopnlem  47046  ovnsubaddlem2  47313  smfinflem  47559  fsupdm  47584  finfdm  47588  eluzge0nn0  48077  fzopredsuc  48089  imasetpreimafvbijlemfv  48179  lighneallem4  48390  oexpnegALTV  48470  oexpnegnz  48471  tgblthelfgott  48608  clnbgrgrim  48727  isubgr3stgrlem3  48761  rmsupp0  49176  rmsuppss  49178  lincresunit3lem3  49282  lincresunit3lem2  49288  lindssnlvec  49294  fdivmptf  49349  refdivmptf  49350  elbigolo1  49365  rrx2linest  49550  itsclc0lem1  49564  itsclc0lem2  49565  itsclc0yqsollem1  49570  itsclc0b  49580  setc1onsubc  50408