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  3582  2nreu  4385  f1prex  7230  weniso  7300  ofmpteq  7645  tfisi  7801  mposn  8044  fprlem1  8241  smogt  8298  smocdmdom  8299  omeulem1  8508  nnmord  8559  nnmword  8560  naddasslem1  8621  naddasslem2  8622  difsnen  8988  enfixsn  9015  mapunen  9075  ac6sfi  9185  ordiso2  9421  wemaplem2  9453  wemapso2lem  9458  en2eqpr  9918  acndom  9962  infmap2  10128  cflim2  10174  cfsmolem  10181  coftr  10184  fin23lem26  10236  isf32lem9  10272  fin1a2lem9  10319  fin1a2lem10  10320  gchdomtri  10541  canth4  10559  gchpwdom  10582  gruima  10714  grudomon  10729  prn0  10901  distrlem4pr  10938  prlem934  10945  addcan  11319  addcan2  11320  divmulass  11821  divmulasscom  11822  ltmul1a  11993  supmul1  12114  uzsupss  12879  xaddass  13190  xleadd1a  13194  xlesubadd  13204  xmulass  13228  xlemul2a  13230  xadddilem  13235  xadddi  13236  ixxdisj  13302  ixxun  13303  ixxlb  13309  icoshftf1o  13416  icodisj  13418  ioounsn  13419  lincmb01cmp  13437  iccf1o  13438  elfz1b  13536  ssfzoulel  13704  fzoopth  13706  modmuladd  13864  modaddmulmod  13889  ltexp2a  14117  leexp2  14122  ltexp2r  14124  exple1  14128  expnlbnd2  14185  mulsubdivbinom2  14213  fun2dmnop0  14455  ccatass  14540  ccatopth  14667  pfxccatin12lem2a  14678  repswpfx  14736  repswccat  14737  cshwidxmodr  14755  2cshw  14764  repsco  14791  s2f1o  14867  limsupgle  15428  limsupgre  15432  addcn2  15545  mulcn2  15547  binomrisefac  15996  dvdsval2  16213  dvdsadd2b  16264  dvdsmod  16287  oexpneg  16303  sadass  16429  gcdass  16505  rplpwr  16516  lcmass  16572  coprmdvds2  16612  rpmulgcd2  16614  rpdvds  16618  coprmprod  16619  cncongr2  16626  rpexp  16681  prmdiveq  16745  hashgcdlem  16747  odzdvds  16755  coprimeprodsq2  16769  pythagtriplem3  16778  pythagtriplem4  16779  pcdvdsb  16829  vdwnnlem1  16955  0ram  16980  ramz2  16984  ramub1lem1  16986  mremre  17555  mrieqv2d  17594  lubss  18468  lubun  18470  clatleglb  18473  clatglbss  18474  mrelatglb  18515  isnsgrp  18680  issubmnd  18718  gsumccat  18798  frmdss2  18820  submefmnd  18852  nmzsubg  19129  ghmnsgima  19204  gsmsymgreqlem1  19394  psgnunilem4  19461  odmodnn0  19504  odnncl  19509  odmod  19510  oddvds  19511  odeq  19514  odmulgid  19518  odmulgeq  19521  odbezout  19522  odf1o1  19536  odf1o2  19537  odngen  19541  gexdvdsi  19547  pgpfi1  19559  odcau  19568  subgslw  19580  fislw  19589  lsmless1x  19608  lsmless2x  19609  lsmsubm  19617  lsmmod  19639  lsmmod2  19640  efgsfo  19703  odadd1  19812  odadd2  19813  odadd  19814  lsmcomx  19820  prdscmnd  19825  gsumconst  19898  ablsimpgfindlem1  20073  srg1zr  20185  csrgbinom  20202  ring1eq0  20268  mulgass2  20279  rngisom1  20435  rhmdvdsr  20474  cntzsubrng  20533  cntzsubr  20572  isabvd  20778  rmodislmod  20914  0lmhm  21025  lmhmvsca  21030  reslmhm2b  21039  pwssplit1  21044  pwssplit2  21045  pwssplit3  21046  lbspss  21067  lspsnat  21133  lidldvgen  21322  xrsdsreclblem  21400  cssmre  21681  obs2ss  21717  uvcresum  21781  frlmsslsp  21784  frlmup4  21789  lindff1  21808  f1lindf  21810  lsslindf  21818  islindf4  21826  issubassa  21855  evlsval2  22074  coe1subfv  22240  coe1sclmul  22256  coe1sclmul2  22258  mpomatmul  22420  mamutpos  22432  scmatscmide  22481  mavmulsolcl  22525  mulmarep1gsum2  22548  mdetdiaglem  22572  mdetdiag  22573  mdetunilem1  22586  mdetunilem3  22588  mdetunilem9  22594  maducoeval2  22614  madurid  22618  slesolinvbi  22655  cramerimplem1  22657  cramerlem1  22661  cramer  22665  cpmatel2  22687  m2cpm  22715  m2pmfzmap  22721  m2cpminvid2lem  22728  m2cpminvid2  22729  decpmatmul  22746  pmatcollpw1lem2  22749  pmatcollpw1  22750  pmatcollpw2lem  22751  pmatcollpwfi  22756  pm2mpcl  22771  mply1topmatcl  22779  mp2pm2mplem2  22781  mp2pm2mplem4  22783  mp2pm2mplem5  22784  mp2pm2mp  22785  pm2mpghmlem2  22786  pm2mpghmlem1  22787  chfacfisfcpmat  22829  topssnei  23098  cnconst2  23257  cnpresti  23262  cnprest2  23264  cnpdis  23267  cnt0  23320  cnt1  23324  cnhaus  23328  sscmp  23379  hauscmp  23381  cnconn  23396  unconn  23403  finlocfin  23494  comppfsc  23506  kgen2ss  23529  ptpjopn  23586  prdstopn  23602  ptrescn  23613  qtopss  23689  kqfvima  23704  fbssint  23812  fbasrn  23858  filuni  23859  fmss  23920  rnelfm  23927  fmufil  23933  fmco  23935  flimss2  23946  flimss1  23947  flimrest  23957  cnpflf2  23974  flfcnp  23978  supnfcls  23994  fclsss1  23996  fclsss2  23997  isfcf  24008  subgntr  24081  opnsubg  24082  cldsubg  24085  ghmcnp  24089  ustuqtop1  24215  bldisj  24372  blgt0  24373  bl2in  24374  blss2ps  24377  blss2  24378  blssps  24398  blss  24399  xmetresbl  24411  lpbl  24477  blcld  24479  stdbdmopn  24492  metcnp3  24514  metcnp  24515  metcnp2  24516  txmetcnp  24521  blval2  24536  nmoix  24703  nmoi2  24704  nmotri  24713  metdsge  24824  metdseq0  24829  iocopnst  24916  xrhmeo  24922  nmhmcn  25096  cphsqrtcl2  25162  cphsqrtcl3  25163  cssbn  25351  pjth  25415  ovoliunlem2  25479  volun  25521  mbfimaopn2  25633  iblconst  25794  limcvallem  25847  dvfval  25873  dvcnp2  25896  dvcn  25897  deg1mul3le  26094  deg1tmle  26095  dvdsq1p  26140  idomrootle  26150  ig1peu  26152  ig1pdvds  26157  ply1term  26181  coeid3  26217  dgrmulc  26248  dvply1  26262  aaliou2  26319  efcvx  26430  tanord  26518  eflogeq  26582  logdivlti  26600  logccv  26643  recxpcl  26655  cxplea  26676  cxpeq  26738  ang180  26795  isosctrlem2  26800  cxp2lim  26958  amgm  26972  muval1  27114  dvdssqf  27119  mumullem2  27161  mumul  27162  bcmono  27259  lgsneg  27303  lgsdilem  27306  lgsdirprm  27313  lgsdir  27314  lgsdi  27316  lgsne0  27317  nolesgn2o  27654  nogesgn1o  27656  nosep1o  27664  nosep2o  27665  nosepssdm  27669  nosupres  27690  nosupbnd1lem1  27691  nosupbnd1lem4  27694  nosupbnd1lem5  27695  nosupbnd1lem6  27696  noinfres  27705  noinfbnd1lem1  27706  noinfbnd1lem4  27709  noinfbnd1lem6  27711  noinfbnd2  27714  noetasuplem3  27718  noetainflem3  27722  leslss  27920  cofslts  27929  coinitslts  27930  cofcutrtime  27938  addsass  28016  addsdi  28166  mulsass  28177  ltmuls2  28182  divmulsw  28204  bdayfinbndlem1  28478  z12bdaylem  28495  brbtwn2  28993  colinearalglem1  28994  colinearalg  28998  axcgrtr  29003  axsegconlem8  29012  axsegconlem9  29013  axsegconlem10  29014  axcontlem2  29053  axcontlem10  29061  elntg2  29073  ewlkle  29694  crctcshwlkn0lem5  29902  wwlknp  29931  wwlksnext  29981  wwlksnextproplem1  29997  wspthsnwspthsnon  30004  clwlkclwwlklem3  30091  erclwwlksym  30111  erclwwlknsym  30160  upgriseupth  30297  eucrct2eupth  30335  3cyclfrgrrn  30376  numclwwlk2lem1lem  30432  numclwwlk1lem2foa  30444  frgrregord13  30486  nvmul0or  30741  ipval2lem2  30795  lnoadd  30849  lnosub  30850  lnomul  30851  shless  31450  shlej1  31451  kbmul  32046  homco2  32068  kbass2  32208  eliccelico  32870  elicoelioo  32871  iocinioc2  32872  iocinif  32874  difioo  32875  nexple  32937  swrdrn2  33034  swrdrn3  33035  xrge0adddir  33098  xrge0npcan  33100  isarchi2  33266  archiabl  33279  pidlnz  33456  lindssn  33458  ssmxidl  33554  pstmfval  34061  fmcncfil  34096  zrhnm  34132  qqhnm  34155  volfiniune  34395  dya2iocnrect  34446  probinc  34586  cndprob01  34600  signswmnd  34722  bnj517  35048  cvmsss2  35477  cvmlift2lem10  35515  br6  35960  funsseq  35971  cgrtriv  36205  5segofs  36209  btwnouttr2  36225  btwnxfr  36259  lineext  36279  btwnconn1lem13  36302  brsegle2  36312  nn0prpwlem  36525  weiunpo  36668  weiunso  36669  weiunfr  36670  weiunse  36671  axtcond  36681  lindsenlbs  37947  blbnd  38119  ismtyima  38135  rrndstprj2  38163  ghomdiv  38224  grpokerinj  38225  lsatfixedN  39466  lssat  39473  lshpkrlem4  39570  cvrcon3b  39734  atlen0  39767  atcvreq0  39771  atnle  39774  atlatmstc  39776  atlatle  39777  cvlcvr1  39796  hlsupr2  39844  hlrelat2  39860  cvrexchlem  39876  lnnat  39884  atcvrj2b  39889  3dimlem3  39918  3dim1  39924  1cvrjat  39932  llni  39965  llni2  39969  llnexatN  39978  2llnmat  39981  lplni  39989  2atnelpln  40001  llncvrlpln2  40014  2llnmj  40017  lplnexatN  40020  lplnexllnN  40021  2llnm3N  40026  lvoli  40032  lvoli3  40034  lvolnle3at  40039  islvol2aN  40049  4atlem4a  40056  4atlem4b  40057  4atlem11  40066  lplncvrlvol2  40072  2lplnmj  40079  islinei  40197  linepmap  40232  lnjatN  40237  lncvrat  40239  lncmp  40240  elpaddn0  40257  elpaddatriN  40260  elpaddat  40261  paddcom  40270  paddss2  40275  paddss12  40276  paddasslem4  40280  paddasslem9  40285  paddasslem10  40286  pmodl42N  40308  pmapjoin  40309  llnmod1i2  40317  polcon2bN  40377  pclfinclN  40407  poml4N  40410  poml6N  40412  osumcllem1N  40413  osumcllem2N  40414  osumcllem11N  40423  osumclN  40424  pmapojoinN  40425  pexmidlem2N  40428  pexmidlem3N  40429  pexmidlem4N  40430  pexmidlem6N  40432  pexmidlem7N  40433  pl42lem2N  40437  pl42lem3N  40438  pl42lem4N  40439  pl42N  40440  lhprelat3N  40497  4atex  40533  lauteq  40552  lautco  40554  ltrncoidN  40585  ltrneq2  40605  ltrnideq  40632  trlnle  40643  trlval3  40644  cdlemc  40654  cdlemd9  40663  cdlemd  40664  cdleme21j  40793  cdleme21  40794  cdleme29ex  40831  cdlemefr27cl  40860  cdlemefs27cl  40870  cdleme32d  40901  cdleme32f  40903  cdleme35h2  40914  cdleme40m  40924  cdleme17d3  40953  cdleme48fvg  40957  cdlemeg46fvcl  40963  cdlemeg46fgN  40991  cdleme48fgv  40995  cdleme50trn3  41010  cdlemb3  41063  cdlemg8  41088  cdlemg11a  41094  cdlemg15a  41112  cdlemg15  41113  cdlemg16  41114  cdlemg16z  41116  cdlemg17dN  41120  cdlemg24  41145  cdlemg37  41146  cdlemg29  41162  cdlemg33b  41164  cdlemg38  41172  cdlemg40  41174  trlco  41184  cdlemg44b  41189  ltrncom  41195  trljco  41197  tendococl  41229  tendoplcl  41238  tendoplcom  41239  cdlemj2  41279  tendoid0  41282  tendo1ne0  41285  cdlemk25-3  41361  cdlemk36  41370  cdlemkid4  41391  cdlemk19x  41400  cdlemk53  41414  cdlemk56  41428  cdleml5N  41437  tendospcanN  41480  cdlemm10N  41575  dihord6apre  41713  dihord  41721  dihmeetlem1N  41747  dihglblem2N  41751  dihmeetlem2N  41756  dihmeetbN  41760  dihmeetlem5  41765  dihmeetlem6  41766  dihmeetlem7N  41767  dihmeetlem10N  41773  dihmeetlem12N  41775  dihmeetlem16N  41779  dihmeetlem17N  41780  dihmeetlem18N  41781  dihmeetALTN  41784  dihlspsnssN  41789  dvh3dim2  41905  dvh3dim3N  41906  lcfrlem16  42015  mapdrvallem2  42102  mapdh8ad  42236  hgmapvvlem3  42382  sticksstones1  42596  sticksstones2  42597  aks6d1c6isolem1  42624  resubcan2  42831  diophrw  43202  eldioph2lem1  43203  diophrex  43218  rencldnfi  43264  pellexlem2  43273  pellqrexplicit  43320  infmrgelbi  43321  pellfundglb  43328  pellfund14gap  43330  rmxycomplete  43360  congadd  43409  acongeq  43426  jm2.19  43436  jm2.23  43439  jm2.20nn  43440  jm2.27  43451  jm3.1  43463  lnmepi  43528  lmhmlnmsplit  43530  hbtlem2  43567  dgraa0p  43592  proot1hash  43638  iocunico  43654  iocinico  43655  oasubex  43729  cantnf2  43768  onmcl  43774  omcl2  43776  nadd2rabex  43829  nadd1rabtr  43831  nadd1rabex  43833  fzunt  43897  relexpxpmin  44159  ntrclsk3  44512  grur1cld  44674  ismnu  44703  grumnudlem  44727  ismnushort  44743  rfcnnnub  45482  uzwo4  45499  wessf1ornlem  45630  supxrge  45783  infleinflem2  45815  iccintsng  45968  climsuse  46053  lptre2pt  46083  limcleqr  46087  0ellimcdiv  46092  fnlimfvre  46117  dvnprodlem1  46389  volioc  46415  stoweidlem17  46460  stoweidlem19  46462  stoweidlem20  46463  stoweidlem22  46465  stoweidlem28  46471  stoweidlem34  46477  stoweidlem44  46487  stoweidlem60  46503  wallispilem3  46510  fourierdlem42  46592  fourierdlem48  46597  fourierdlem51  46600  fourierdlem54  46603  fourierdlem74  46623  fourierdlem77  46626  fourierdlem87  46636  fourierdlem97  46646  ioorrnopnlem  46747  ovnsubaddlem2  47014  smfinflem  47260  fsupdm  47285  finfdm  47289  eluzge0nn0  47757  fzopredsuc  47769  imasetpreimafvbijlemfv  47859  lighneallem4  48070  oexpnegALTV  48150  oexpnegnz  48151  tgblthelfgott  48288  clnbgrgrim  48407  isubgr3stgrlem3  48441  rmsupp0  48841  rmsuppss  48843  lincresunit3lem3  48947  lincresunit3lem2  48953  lindssnlvec  48959  fdivmptf  49014  refdivmptf  49015  elbigolo1  49030  rrx2linest  49215  itsclc0lem1  49229  itsclc0lem2  49230  itsclc0yqsollem1  49235  itsclc0b  49245  setc1onsubc  50074