Theorem simpl2 1199

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpl12  1256  simpl22  1259  simpl32  1262  simp1l2  1274  simp2l2  1280  simp3l2  1286  3anandirs  1480  rspc3ev  3584  2nreu  4379  f1prex  7235  weniso  7305  ofmpteq  7650  tfisi  7806  mposn  8049  fprlem1  8247  smogt  8304  smocdmdom  8305  omeulem1  8514  nnmord  8565  nnmword  8566  naddasslem1  8627  naddasslem2  8628  difsnen  8994  enfixsn  9021  mapunen  9081  ac6sfi  9191  ordiso2  9427  wemaplem2  9459  wemapso2lem  9464  en2eqpr  9927  acndom  9971  infmap2  10137  cflim2  10183  cfsmolem  10190  coftr  10193  fin23lem26  10245  isf32lem9  10281  fin1a2lem9  10328  fin1a2lem10  10329  gchdomtri  10550  canth4  10568  gchpwdom  10591  gruima  10723  grudomon  10738  prn0  10910  distrlem4pr  10947  prlem934  10954  addcan  11328  addcan2  11329  divmulass  11830  divmulasscom  11831  ltmul1a  12002  supmul1  12123  uzsupss  12888  xaddass  13199  xleadd1a  13203  xlesubadd  13213  xmulass  13237  xlemul2a  13239  xadddilem  13244  xadddi  13245  ixxdisj  13311  ixxun  13312  ixxlb  13318  icoshftf1o  13425  icodisj  13427  ioounsn  13428  lincmb01cmp  13446  iccf1o  13447  elfz1b  13545  ssfzoulel  13713  fzoopth  13715  modmuladd  13873  modaddmulmod  13898  ltexp2a  14126  leexp2  14131  ltexp2r  14133  exple1  14137  expnlbnd2  14194  mulsubdivbinom2  14222  fun2dmnop0  14464  ccatass  14549  ccatopth  14676  pfxccatin12lem2a  14687  repswpfx  14745  repswccat  14746  cshwidxmodr  14764  2cshw  14773  repsco  14800  s2f1o  14876  limsupgle  15437  limsupgre  15441  addcn2  15554  mulcn2  15556  binomrisefac  16005  dvdsval2  16222  dvdsadd2b  16273  dvdsmod  16296  oexpneg  16312  sadass  16438  gcdass  16514  rplpwr  16525  lcmass  16581  coprmdvds2  16621  rpmulgcd2  16623  rpdvds  16627  coprmprod  16628  cncongr2  16635  rpexp  16690  prmdiveq  16754  hashgcdlem  16756  odzdvds  16764  coprimeprodsq2  16778  pythagtriplem3  16787  pythagtriplem4  16788  pcdvdsb  16838  vdwnnlem1  16964  0ram  16989  ramz2  16993  ramub1lem1  16995  mremre  17564  mrieqv2d  17603  lubss  18477  lubun  18479  clatleglb  18482  clatglbss  18483  mrelatglb  18524  isnsgrp  18689  issubmnd  18727  gsumccat  18807  frmdss2  18829  submefmnd  18861  nmzsubg  19138  ghmnsgima  19213  gsmsymgreqlem1  19403  psgnunilem4  19470  odmodnn0  19513  odnncl  19518  odmod  19519  oddvds  19520  odeq  19523  odmulgid  19527  odmulgeq  19530  odbezout  19531  odf1o1  19545  odf1o2  19546  odngen  19550  gexdvdsi  19556  pgpfi1  19568  odcau  19577  subgslw  19589  fislw  19598  lsmless1x  19617  lsmless2x  19618  lsmsubm  19626  lsmmod  19648  lsmmod2  19649  efgsfo  19712  odadd1  19821  odadd2  19822  odadd  19823  lsmcomx  19829  prdscmnd  19834  gsumconst  19907  ablsimpgfindlem1  20082  srg1zr  20194  csrgbinom  20211  ring1eq0  20277  mulgass2  20288  rngisom1  20444  rhmdvdsr  20487  cntzsubrng  20546  cntzsubr  20585  isabvd  20791  rmodislmod  20927  0lmhm  21037  lmhmvsca  21042  reslmhm2b  21051  pwssplit1  21056  pwssplit2  21057  pwssplit3  21058  lbspss  21079  lspsnat  21145  lidldvgen  21334  xrsdsreclblem  21395  cssmre  21675  obs2ss  21711  uvcresum  21775  frlmsslsp  21778  frlmup4  21783  lindff1  21802  f1lindf  21804  lsslindf  21812  islindf4  21820  issubassa  21849  evlsval2  22070  coe1subfv  22259  coe1sclmul  22275  coe1sclmul2  22277  mpomatmul  22436  mamutpos  22448  scmatscmide  22497  mavmulsolcl  22541  mulmarep1gsum2  22564  mdetdiaglem  22588  mdetdiag  22589  mdetunilem1  22602  mdetunilem3  22604  mdetunilem9  22610  maducoeval2  22630  madurid  22634  slesolinvbi  22671  cramerimplem1  22673  cramerlem1  22677  cramer  22681  cpmatel2  22703  m2cpm  22731  m2pmfzmap  22737  m2cpminvid2lem  22744  m2cpminvid2  22745  decpmatmul  22762  pmatcollpw1lem2  22765  pmatcollpw1  22766  pmatcollpw2lem  22767  pmatcollpwfi  22772  pm2mpcl  22787  mply1topmatcl  22795  mp2pm2mplem2  22797  mp2pm2mplem4  22799  mp2pm2mplem5  22800  mp2pm2mp  22801  pm2mpghmlem2  22802  pm2mpghmlem1  22803  chfacfisfcpmat  22845  topssnei  23114  cnconst2  23273  cnpresti  23278  cnprest2  23280  cnpdis  23283  cnt0  23336  cnt1  23340  cnhaus  23344  sscmp  23395  hauscmp  23397  cnconn  23412  unconn  23419  finlocfin  23510  comppfsc  23522  kgen2ss  23545  ptpjopn  23602  prdstopn  23618  ptrescn  23629  qtopss  23705  kqfvima  23720  fbssint  23828  fbasrn  23874  filuni  23875  fmss  23936  rnelfm  23943  fmufil  23949  fmco  23951  flimss2  23962  flimss1  23963  flimrest  23973  cnpflf2  23990  flfcnp  23994  supnfcls  24010  fclsss1  24012  fclsss2  24013  isfcf  24024  subgntr  24097  opnsubg  24098  cldsubg  24101  ghmcnp  24105  ustuqtop1  24231  bldisj  24388  blgt0  24389  bl2in  24390  blss2ps  24393  blss2  24394  blssps  24414  blss  24415  xmetresbl  24427  lpbl  24493  blcld  24495  stdbdmopn  24508  metcnp3  24530  metcnp  24531  metcnp2  24532  txmetcnp  24537  blval2  24552  nmoix  24719  nmoi2  24720  nmotri  24729  metdsge  24840  metdseq0  24845  iocopnst  24932  xrhmeo  24938  nmhmcn  25112  cphsqrtcl2  25178  cphsqrtcl3  25179  cssbn  25367  pjth  25431  ovoliunlem2  25495  volun  25537  mbfimaopn2  25649  iblconst  25810  limcvallem  25863  dvfval  25889  dvcnp2  25912  dvcn  25913  deg1mul3le  26107  deg1tmle  26108  dvdsq1p  26153  idomrootle  26163  ig1peu  26165  ig1pdvds  26170  ply1term  26194  coeid3  26230  dgrmulc  26261  dvply1  26275  aaliou2  26331  efcvx  26439  tanord  26527  eflogeq  26591  logdivlti  26609  logccv  26652  recxpcl  26664  cxplea  26685  cxpeq  26746  ang180  26803  isosctrlem2  26808  cxp2lim  26965  amgm  26979  muval1  27121  dvdssqf  27126  mumullem2  27168  mumul  27169  bcmono  27265  lgsneg  27309  lgsdilem  27312  lgsdirprm  27319  lgsdir  27320  lgsdi  27322  lgsne0  27323  nolesgn2o  27660  nogesgn1o  27662  nosep1o  27670  nosep2o  27671  nosepssdm  27675  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  noinfres  27711  noinfbnd1lem1  27712  noinfbnd1lem4  27715  noinfbnd1lem6  27717  noinfbnd2  27720  noetasuplem3  27724  noetainflem3  27728  leslss  27926  cofslts  27935  coinitslts  27936  cofcutrtime  27944  addsass  28022  addsdi  28172  mulsass  28183  ltmuls2  28188  divmulsw  28210  bdayfinbndlem1  28484  z12bdaylem  28501  brbtwn2  28999  colinearalglem1  29000  colinearalg  29004  axcgrtr  29009  axsegconlem8  29018  axsegconlem9  29019  axsegconlem10  29020  axcontlem2  29059  axcontlem10  29067  elntg2  29079  ewlkle  29699  crctcshwlkn0lem5  29907  wwlknp  29936  wwlksnext  29986  wwlksnextproplem1  30002  wspthsnwspthsnon  30009  clwlkclwwlklem3  30096  erclwwlksym  30116  erclwwlknsym  30165  upgriseupth  30302  eucrct2eupth  30340  3cyclfrgrrn  30381  numclwwlk2lem1lem  30437  numclwwlk1lem2foa  30449  frgrregord13  30491  nvmul0or  30746  ipval2lem2  30800  lnoadd  30854  lnosub  30855  lnomul  30856  shless  31455  shlej1  31456  kbmul  32051  homco2  32073  kbass2  32213  eliccelico  32876  elicoelioo  32877  iocinioc2  32878  iocinif  32880  difioo  32881  nexple  32943  swrdrn2  33040  swrdrn3  33041  xrge0adddir  33104  xrge0npcan  33106  isarchi2  33273  archiabl  33286  pidlnz  33466  lindssn  33468  ssmxidl  33564  pstmfval  34087  fmcncfil  34122  zrhnm  34158  qqhnm  34181  volfiniune  34421  dya2iocnrect  34472  probinc  34612  cndprob01  34626  signswmnd  34748  bnj517  35074  cvmsss2  35503  cvmlift2lem10  35541  br6  35986  funsseq  35997  cgrtriv  36231  5segofs  36235  btwnouttr2  36251  btwnxfr  36285  lineext  36305  btwnconn1lem13  36328  brsegle2  36338  nn0prpwlem  36551  weiunpo  36694  weiunso  36695  weiunfr  36696  weiunse  36697  axtcond  36707  lindsenlbs  37983  blbnd  38155  ismtyima  38171  rrndstprj2  38199  ghomdiv  38260  grpokerinj  38261  lsatfixedN  39502  lssat  39509  lshpkrlem4  39606  cvrcon3b  39770  atlen0  39803  atcvreq0  39807  atnle  39810  atlatmstc  39812  atlatle  39813  cvlcvr1  39832  hlsupr2  39880  hlrelat2  39896  cvrexchlem  39912  lnnat  39920  atcvrj2b  39925  3dimlem3  39954  3dim1  39960  1cvrjat  39968  llni  40001  llni2  40005  llnexatN  40014  2llnmat  40017  lplni  40025  2atnelpln  40037  llncvrlpln2  40050  2llnmj  40053  lplnexatN  40056  lplnexllnN  40057  2llnm3N  40062  lvoli  40068  lvoli3  40070  lvolnle3at  40075  islvol2aN  40085  4atlem4a  40092  4atlem4b  40093  4atlem11  40102  lplncvrlvol2  40108  2lplnmj  40115  islinei  40233  linepmap  40268  lnjatN  40273  lncvrat  40275  lncmp  40276  elpaddn0  40293  elpaddatriN  40296  elpaddat  40297  paddcom  40306  paddss2  40311  paddss12  40312  paddasslem4  40316  paddasslem9  40321  paddasslem10  40322  pmodl42N  40344  pmapjoin  40345  llnmod1i2  40353  polcon2bN  40413  pclfinclN  40443  poml4N  40446  poml6N  40448  osumcllem1N  40449  osumcllem2N  40450  osumcllem11N  40459  osumclN  40460  pmapojoinN  40461  pexmidlem2N  40464  pexmidlem3N  40465  pexmidlem4N  40466  pexmidlem6N  40468  pexmidlem7N  40469  pl42lem2N  40473  pl42lem3N  40474  pl42lem4N  40475  pl42N  40476  lhprelat3N  40533  4atex  40569  lauteq  40588  lautco  40590  ltrncoidN  40621  ltrneq2  40641  ltrnideq  40668  trlnle  40679  trlval3  40680  cdlemc  40690  cdlemd9  40699  cdlemd  40700  cdleme21j  40829  cdleme21  40830  cdleme29ex  40867  cdlemefr27cl  40896  cdlemefs27cl  40906  cdleme32d  40937  cdleme32f  40939  cdleme35h2  40950  cdleme40m  40960  cdleme17d3  40989  cdleme48fvg  40993  cdlemeg46fvcl  40999  cdlemeg46fgN  41027  cdleme48fgv  41031  cdleme50trn3  41046  cdlemb3  41099  cdlemg8  41124  cdlemg11a  41130  cdlemg15a  41148  cdlemg15  41149  cdlemg16  41150  cdlemg16z  41152  cdlemg17dN  41156  cdlemg24  41181  cdlemg37  41182  cdlemg29  41198  cdlemg33b  41200  cdlemg38  41208  cdlemg40  41210  trlco  41220  cdlemg44b  41225  ltrncom  41231  trljco  41233  tendococl  41265  tendoplcl  41274  tendoplcom  41275  cdlemj2  41315  tendoid0  41318  tendo1ne0  41321  cdlemk25-3  41397  cdlemk36  41406  cdlemkid4  41427  cdlemk19x  41436  cdlemk53  41450  cdlemk56  41464  cdleml5N  41473  tendospcanN  41516  cdlemm10N  41611  dihord6apre  41749  dihord  41757  dihmeetlem1N  41783  dihglblem2N  41787  dihmeetlem2N  41792  dihmeetbN  41796  dihmeetlem5  41801  dihmeetlem6  41802  dihmeetlem7N  41803  dihmeetlem10N  41809  dihmeetlem12N  41811  dihmeetlem16N  41815  dihmeetlem17N  41816  dihmeetlem18N  41817  dihmeetALTN  41820  dihlspsnssN  41825  dvh3dim2  41941  dvh3dim3N  41942  lcfrlem16  42051  mapdrvallem2  42138  mapdh8ad  42272  hgmapvvlem3  42418  sticksstones1  42632  sticksstones2  42633  aks6d1c6isolem1  42660  resubcan2  42866  diophrw  43209  eldioph2lem1  43210  diophrex  43225  rencldnfi  43267  pellexlem2  43276  pellqrexplicit  43323  infmrgelbi  43324  pellfundglb  43331  pellfund14gap  43333  rmxycomplete  43363  congadd  43412  acongeq  43429  jm2.19  43439  jm2.23  43442  jm2.20nn  43443  jm2.27  43454  jm3.1  43466  lnmepi  43531  lmhmlnmsplit  43533  hbtlem2  43570  dgraa0p  43595  proot1hash  43641  iocunico  43657  iocinico  43658  oasubex  43732  cantnf2  43771  onmcl  43777  omcl2  43779  nadd2rabex  43832  nadd1rabtr  43834  nadd1rabex  43836  fzunt  43900  relexpxpmin  44162  ntrclsk3  44515  grur1cld  44677  ismnu  44706  grumnudlem  44730  ismnushort  44746  rfcnnnub  45485  uzwo4  45502  wessf1ornlem  45633  supxrge  45784  infleinflem2  45816  iccintsng  45969  climsuse  46054  lptre2pt  46084  limcleqr  46088  0ellimcdiv  46093  fnlimfvre  46118  dvnprodlem1  46390  volioc  46416  stoweidlem17  46461  stoweidlem19  46463  stoweidlem20  46464  stoweidlem22  46466  stoweidlem28  46472  stoweidlem34  46478  stoweidlem44  46488  stoweidlem60  46504  wallispilem3  46511  fourierdlem42  46593  fourierdlem48  46598  fourierdlem51  46601  fourierdlem54  46604  fourierdlem74  46624  fourierdlem77  46627  fourierdlem87  46637  fourierdlem97  46647  ioorrnopnlem  46748  ovnsubaddlem2  47015  smfinflem  47261  fsupdm  47286  finfdm  47290  eluzge0nn0  47776  fzopredsuc  47788  imasetpreimafvbijlemfv  47878  lighneallem4  48089  oexpnegALTV  48169  oexpnegnz  48170  tgblthelfgott  48307  clnbgrgrim  48426  isubgr3stgrlem3  48460  rmsupp0  48860  rmsuppss  48862  lincresunit3lem3  48966  lincresunit3lem2  48972  lindssnlvec  48978  fdivmptf  49033  refdivmptf  49034  elbigolo1  49049  rrx2linest  49234  itsclc0lem1  49248  itsclc0lem2  49249  itsclc0yqsollem1  49254  itsclc0b  49264  setc1onsubc  50093