Theorem simpl2 1211

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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 402  df-3an 1105

This theorem is used by:  simpl12  1268  simpl22  1271  simpl32  1274  simp1l2  1286  simp2l2  1292  simp3l2  1298  3anandirs  1501  rspc3ev  3592  2nreu  4401  f1prex  7280  weniso  7352  ofmpteq  7699  tfisi  7853  mposn  8097  fprlem1  8296  smogt  8353  smocdmdom  8354  omeulem1  8568  nnmord  8619  nnmword  8620  naddasslem1  8682  naddasslem2  8683  difsnen  9056  enfixsn  9083  mapunen  9143  ac6sfi  9253  ordiso2  9487  wemaplem2  9519  wemapso2lem  9524  en2eqpr  10058  acndom  10102  infmap2  10267  cflim2  10313  cfsmolem  10320  coftr  10323  fin23lem26  10375  isf32lem9  10411  fin1a2lem9  10458  fin1a2lem10  10459  gchdomtri  10686  canth4  10704  gchpwdom  10727  gruima  10859  grudomon  10874  prn0  11046  distrlem4pr  11083  prlem934  11090  addcan  11466  addcan2  11467  divmulass  11967  divmulasscom  11968  ltmul1a  12136  supmul1  12256  uzsupss  13037  xaddass  13349  xleadd1a  13353  xlesubadd  13363  xmulass  13387  xlemul2a  13389  xadddilem  13394  xadddi  13395  ixxdisj  13461  ixxun  13462  ixxlb  13468  icoshftf1o  13575  icodisj  13577  ioounsn  13578  lincmb01cmp  13596  iccf1o  13597  elfz1b  13696  ssfzoulel  13864  fzoopth  13866  modmuladd  14025  modaddmulmod  14050  ltexp2a  14278  leexp2  14283  ltexp2r  14285  exple1  14289  expnlbnd2  14346  mulsubdivbinom2  14374  fun2dmnop0  14617  ccatass  14702  swrdrn3  14770  ccatopth  14833  pfxccatin12lem2a  14844  repswpfx  14904  repswccat  14905  cshwidxmodr  14923  2cshw  14932  repsco  14959  s2f1o  15035  limsupgle  15612  limsupgre  15616  addcn2  15729  mulcn2  15731  binomrisefac  16176  dvdsval2  16393  dvdsadd2b  16444  dvdsmod  16467  oexpneg  16483  sadass  16609  gcdass  16685  rplpwr  16696  lcmass  16752  coprmdvds2  16792  rpmulgcd2  16794  rpdvds  16798  coprmprod  16799  cncongr2  16806  rpexp  16861  prmdiveq  16925  hashgcdlem  16927  odzdvds  16935  coprimeprodsq2  16949  pythagtriplem3  16958  pythagtriplem4  16959  pcdvdsb  17009  vdwnnlem1  17135  0ram  17160  ramz2  17164  ramub1lem1  17166  mremre  17736  mrieqv2d  17775  lubss  18649  lubun  18651  clatleglb  18654  clatglbss  18655  mrelatglb  18696  isnsgrp  18874  issubmnd  18915  gsumccat  18999  frmdss2  19021  submefmnd  19053  nmzsubg  19337  ghmnsgima  19416  gsmsymgreqlem1  19606  psgnunilem4  19673  odmodnn0  19716  odnncl  19721  odmod  19722  oddvds  19723  odeq  19726  odmulgid  19730  odmulgeq  19733  odbezout  19734  odf1o1  19748  odf1o2  19749  odngen  19753  gexdvdsi  19759  pgpfi1  19771  odcau  19780  subgslw  19792  fislw  19801  lsmless1x  19820  lsmless2x  19821  lsmsubm  19829  lsmmod  19851  lsmmod2  19852  efgsfo  19915  odadd1  20024  odadd2  20025  odadd  20026  lsmcomx  20032  prdscmnd  20037  gsumconst  20110  ablsimpgfindlem1  20285  csrgbinom  20420  ring1eq0  20491  mulgass2  20502  rngisom1  20658  rhmdvdsr  20720  cntzsubrng  20781  cntzsubr  20820  isdrng3lem2  20968  isabvd  21031  rmodislmod  21167  0lmhm  21277  lmhmvsca  21282  reslmhm2b  21291  pwssplit1  21296  pwssplit2  21297  pwssplit3  21298  lbspss  21319  lspsnat  21385  pidlnz  21490  lidldvgen  21620  xrsdsreclblem  21681  cssmre  21961  obs2ss  21997  uvcresum  22061  frlmsslsp  22064  frlmup4  22069  lindff1  22088  f1lindf  22090  lsslindf  22098  islindf4  22106  lindsenlbs  22119  issubassa  22137  evlsval2  22358  coe1subfv  22547  coe1sclmul  22563  coe1sclmul2  22565  mpomatmul  22723  mamutpos  22735  scmatscmide  22784  mavmulsolcl  22828  mulmarep1gsum2  22851  mdetdiaglem  22875  mdetdiag  22876  mdetunilem1  22889  mdetunilem3  22891  mdetunilem9  22897  maducoeval2  22917  madurid  22921  slesolinvbi  22961  cramerimplem1  22963  cramerlem1  22967  cramer  22971  cpmatel2  22993  m2cpm  23021  m2pmfzmap  23027  m2cpminvid2lem  23034  m2cpminvid2  23035  decpmatmul  23052  pmatcollpw1lem2  23055  pmatcollpw1  23056  pmatcollpw2lem  23057  pmatcollpwfi  23062  pm2mpcl  23077  mply1topmatcl  23085  mp2pm2mplem2  23087  mp2pm2mplem4  23089  mp2pm2mplem5  23090  mp2pm2mp  23091  pm2mpghmlem2  23092  pm2mpghmlem1  23093  chfacfisfcpmat  23135  topssnei  23404  cnconst2  23563  cnpresti  23568  cnprest2  23570  cnpdis  23573  cnt0  23626  cnt1  23630  cnhaus  23634  sscmp  23685  hauscmp  23687  cnconn  23702  unconn  23709  finlocfin  23801  comppfsc  23813  kgen2ss  23836  ptpjopn  23893  prdstopn  23909  ptrescn  23920  qtopss  23996  kqfvima  24011  fbssint  24119  fbasrn  24165  filuni  24166  fmss  24227  rnelfm  24234  fmufil  24240  fmco  24242  flimss2  24253  flimss1  24254  flimrest  24264  cnpflf2  24281  flfcnp  24285  supnfcls  24301  fclsss1  24303  fclsss2  24304  isfcf  24315  subgntr  24388  opnsubg  24389  cldsubg  24392  ghmcnp  24396  ustuqtop1  24522  bldisj  24679  blgt0  24680  bl2in  24681  blss2ps  24684  blss2  24685  blssps  24705  blss  24706  xmetresbl  24718  lpbl  24784  blcld  24786  stdbdmopn  24799  metcnp3  24821  metcnp  24822  metcnp2  24823  txmetcnp  24828  blval2  24843  nmoix  25010  nmoi2  25011  nmotri  25020  metdsge  25131  metdseq0  25136  iocopnst  25223  xrhmeo  25229  nmhmcn  25403  cphsqrtcl2  25469  cphsqrtcl3  25470  cssbn  25658  pjth  25722  ovoliunlem2  25786  volun  25828  mbfimaopn2  25940  iblconst  26100  limcvallem  26153  dvfval  26179  dvcnp2  26202  dvcn  26203  deg1mul3le  26397  deg1tmle  26398  dvdsq1p  26443  idomrootle  26453  ig1peu  26455  ig1pdvds  26460  ply1term  26484  coeid3  26521  dgrmulc  26552  dvply1  26569  aaliou2  26631  efcvx  26740  tanord  26830  eflogeq  26894  logdivlti  26912  logccv  26955  recxpcl  26967  cxplea  26988  cxpeq  27049  ang180  27106  isosctrlem2  27111  cxp2lim  27268  amgm  27282  muval1  27424  dvdssqf  27429  mumullem2  27471  mumul  27472  bcmono  27568  lgsneg  27612  lgsdilem  27615  lgsdirprm  27622  lgsdir  27623  lgsdi  27625  lgsne0  27626  nolesgn2o  27962  nogesgn1o  27964  nosep1o  27972  nosep2o  27973  nosepssdm  27977  nosupres  27998  nosupbnd1lem1  27999  nosupbnd1lem4  28002  nosupbnd1lem5  28003  nosupbnd1lem6  28004  noinfres  28013  noinfbnd1lem1  28014  noinfbnd1lem4  28017  noinfbnd1lem6  28019  noinfbnd2  28022  noetasuplem3  28026  noetainflem3  28030  leslss  28229  cofslts  28238  coinitslts  28239  cofcutrtime  28247  addsass  28325  addsdi  28475  mulsass  28486  ltmuls2  28491  divmulsw  28513  bdayfinbndlem1  28787  z12bdaylem  28804  brbtwn2  29417  colinearalglem1  29418  colinearalg  29422  axcgrtr  29427  axsegconlem8  29436  axsegconlem9  29437  axsegconlem10  29438  axcontlem2  29477  axcontlem10  29485  elntg2  29497  ewlkle  30120  crctcshwlkn0lem5  30337  wwlknp  30366  wwlksnext  30416  wwlksnextproplem1  30432  wspthsnwspthsnon  30439  clwlkclwwlklem3  30526  erclwwlksym  30546  erclwwlknsym  30595  upgriseupth  30742  eucrct2eupth  30780  3cyclfrgrrn  30821  numclwwlk2lem1lem  30877  numclwwlk1lem2foa  30889  frgrregord13  30931  nvmul0or  31186  ipval2lem2  31240  lnoadd  31294  lnosub  31295  lnomul  31296  shless  31895  shlej1  31896  kbmul  32491  homco2  32513  kbass2  32653  eliccelico  33303  elicoelioo  33304  iocinioc2  33305  iocinif  33307  difioo  33308  nexple  33358  swrdrn2  33451  xrge0adddir  33513  xrge0npcan  33515  isarchi2  33680  archiabl  33693  lindssn  33867  ssmxidl  33933  pstmfval  34462  fmcncfil  34497  zrhnm  34533  qqhnm  34556  volfiniune  34797  dya2iocnrect  34848  probinc  34988  cndprob01  35002  signswmnd  35121  bnj517  35450  cvmsss2  35960  cvmlift2lem10  35998  br6  36443  funsseq  36454  cgrtriv  36689  5segofs  36693  btwnouttr2  36709  btwnxfr  36743  lineext  36763  btwnconn1lem13  36786  brsegle2  36796  nmulss1  36885  ltnmul  36887  nmulle  36888  ltnadd  36889  naddle  36890  nadddi  36895  nn0prpwlem  37032  weiunpo  37175  weiunso  37176  weiunfr  37177  weiunse  37178  axtcond  37188  blbnd  38641  ismtyima  38657  rrndstprj2  38685  ghomdiv  38746  grpokerinj  38747  lsatfixedN  39986  lssat  39993  lshpkrlem4  40090  cvrcon3b  40254  atlen0  40287  atcvreq0  40291  atnle  40294  atlatmstc  40296  atlatle  40297  cvlcvr1  40316  hlsupr2  40364  hlrelat2  40380  cvrexchlem  40396  lnnat  40404  atcvrj2b  40409  3dimlem3  40438  3dim1  40444  1cvrjat  40452  llni  40485  llni2  40489  llnexatN  40498  2llnmat  40501  lplni  40509  2atnelpln  40521  llncvrlpln2  40534  2llnmj  40537  lplnexatN  40540  lplnexllnN  40541  2llnm3N  40546  lvoli  40552  lvoli3  40554  lvolnle3at  40559  islvol2aN  40569  4atlem4a  40576  4atlem4b  40577  4atlem11  40586  lplncvrlvol2  40592  2lplnmj  40599  islinei  40717  linepmap  40752  lnjatN  40757  lncvrat  40759  lncmp  40760  elpaddn0  40777  elpaddatriN  40780  elpaddat  40781  paddcom  40790  paddss2  40795  paddss12  40796  paddasslem4  40800  paddasslem9  40805  paddasslem10  40806  pmodl42N  40828  pmapjoin  40829  llnmod1i2  40837  polcon2bN  40897  pclfinclN  40927  poml4N  40930  poml6N  40932  osumcllem1N  40933  osumcllem2N  40934  osumcllem11N  40943  osumclN  40944  pmapojoinN  40945  pexmidlem2N  40948  pexmidlem3N  40949  pexmidlem4N  40950  pexmidlem6N  40952  pexmidlem7N  40953  pl42lem2N  40957  pl42lem3N  40958  pl42lem4N  40959  pl42N  40960  lhprelat3N  41017  4atex  41053  lauteq  41072  lautco  41074  ltrncoidN  41105  ltrneq2  41125  ltrnideq  41152  trlnle  41163  trlval3  41164  cdlemc  41174  cdlemd9  41183  cdlemd  41184  cdleme21j  41313  cdleme21  41314  cdleme29ex  41351  cdlemefr27cl  41380  cdlemefs27cl  41390  cdleme32d  41421  cdleme32f  41423  cdleme35h2  41434  cdleme40m  41444  cdleme17d3  41473  cdleme48fvg  41477  cdlemeg46fvcl  41483  cdlemeg46fgN  41511  cdleme48fgv  41515  cdleme50trn3  41530  cdlemb3  41583  cdlemg8  41608  cdlemg11a  41614  cdlemg15a  41632  cdlemg15  41633  cdlemg16  41634  cdlemg16z  41636  cdlemg17dN  41640  cdlemg24  41665  cdlemg37  41666  cdlemg29  41682  cdlemg33b  41684  cdlemg38  41692  cdlemg40  41694  trlco  41704  cdlemg44b  41709  ltrncom  41715  trljco  41717  tendococl  41749  tendoplcl  41758  tendoplcom  41759  cdlemj2  41799  tendoid0  41802  tendo1ne0  41805  cdlemk25-3  41881  cdlemk36  41890  cdlemkid4  41911  cdlemk19x  41920  cdlemk53  41934  cdlemk56  41948  cdleml5N  41957  tendospcanN  42000  cdlemm10N  42095  dihord6apre  42233  dihord  42241  dihmeetlem1N  42267  dihglblem2N  42271  dihmeetlem2N  42276  dihmeetbN  42280  dihmeetlem5  42285  dihmeetlem6  42286  dihmeetlem7N  42287  dihmeetlem10N  42293  dihmeetlem12N  42295  dihmeetlem16N  42299  dihmeetlem17N  42300  dihmeetlem18N  42301  dihmeetALTN  42304  dihlspsnssN  42309  dvh3dim2  42425  dvh3dim3N  42426  lcfrlem16  42535  mapdrvallem2  42622  mapdh8ad  42756  hgmapvvlem3  42902  sticksstones1  43116  sticksstones2  43117  aks6d1c6isolem1  43144  resubcan2  43367  diophrw  43708  eldioph2lem1  43709  diophrex  43724  rencldnfi  43766  pellexlem2  43775  pellqrexplicit  43822  infmrgelbi  43823  pellfundglb  43830  pellfund14gap  43832  rmxycomplete  43862  congadd  43911  acongeq  43928  jm2.19  43938  jm2.23  43941  jm2.20nn  43942  jm2.27  43953  jm3.1  43965  lnmepi  44030  lmhmlnmsplit  44032  hbtlem2  44069  dgraa0p  44094  proot1hash  44140  iocunico  44156  iocinico  44157  oasubex  44231  cantnf2  44270  onmcl  44276  omcl2  44278  nadd2rabex  44331  nadd1rabtr  44333  nadd1rabex  44335  fzunt  44399  relexpxpmin  44661  ntrclsk3  45014  grur1cld  45174  ismnu  45189  grumnudlem  45213  ismnushort  45229  rfcnnnub  45974  uzwo4  45991  wessf1ornlem  46121  supxrge  46272  infleinflem2  46304  iccintsng  46457  climsuse  46542  lptre2pt  46572  limcleqr  46576  0ellimcdiv  46581  fnlimfvre  46606  dvnprodlem1  46878  volioc  46904  stoweidlem17  46949  stoweidlem19  46951  stoweidlem20  46952  stoweidlem22  46954  stoweidlem28  46960  stoweidlem34  46966  stoweidlem44  46976  stoweidlem60  46992  wallispilem3  46999  fourierdlem42  47081  fourierdlem48  47086  fourierdlem51  47089  fourierdlem54  47092  fourierdlem74  47112  fourierdlem77  47115  fourierdlem87  47125  fourierdlem97  47135  ioorrnopnlem  47236  ovnsubaddlem2  47503  smfinflem  47749  fsupdm  47774  finfdm  47778  eluzge0nn0  48304  fzopredsuc  48316  imasetpreimafvbijlemfv  48406  lighneallem4  48617  oexpnegALTV  48697  oexpnegnz  48698  tgblthelfgott  48835  clnbgrgrim  48954  isubgr3stgrlem3  48988  rmsupp0  49402  rmsuppss  49404  lincresunit3lem3  49508  lincresunit3lem2  49514  lindssnlvec  49520  fdivmptf  49575  refdivmptf  49576  elbigolo1  49591  rrx2linest  49776  itsclc0lem1  49790  itsclc0lem2  49791  itsclc0yqsollem1  49796  itsclc0b  49806  setc1onsubc  50632