Theorem simpl2 1190

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 1184	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  simpl12  1247  simpl22  1250  simpl32  1253  simp1l2  1265  simp2l2  1271  simp3l2  1277  3anandirs  1470  rspc3ev  3566  2nreu  4372  f1prex  7136  weniso  7205  ofmpteq  7533  tfisi  7680  mposn  7914  fprlem1  8087  smogt  8169  smorndom  8170  omeulem1  8375  nnmord  8425  nnmword  8426  difsnen  8794  enfixsn  8821  mapunen  8882  ac6sfi  8988  ordiso2  9204  wemaplem2  9236  wemapso2lem  9241  en2eqpr  9694  acndom  9738  infmap2  9905  cflim2  9950  cfsmolem  9957  coftr  9960  fin23lem26  10012  isf32lem9  10048  fin1a2lem9  10095  fin1a2lem10  10096  gchdomtri  10316  canth4  10334  gchpwdom  10357  gruima  10489  grudomon  10504  prn0  10676  distrlem4pr  10713  prlem934  10720  addcan  11089  addcan2  11090  divmulass  11586  divmulasscom  11587  ltmul1a  11754  supmul1  11874  uzsupss  12609  xaddass  12912  xleadd1a  12916  xlesubadd  12926  xmulass  12950  xlemul2a  12952  xadddilem  12957  xadddi  12958  ixxdisj  13023  ixxun  13024  ixxlb  13030  icoshftf1o  13135  icodisj  13137  ioounsn  13138  lincmb01cmp  13156  iccf1o  13157  elfz1b  13254  ssfzoulel  13409  modmuladd  13561  modaddmulmod  13586  ltexp2a  13812  leexp2  13817  ltexp2r  13819  exple1  13822  expnlbnd2  13877  mulsubdivbinom2  13904  fun2dmnop0  14136  ccatass  14221  ccatopth  14357  pfxccatin12lem2a  14368  repswpfx  14426  repswccat  14427  cshwidxmodr  14445  2cshw  14454  repsco  14481  s2f1o  14557  limsupgle  15114  limsupgre  15118  addcn2  15231  mulcn2  15233  binomrisefac  15680  dvdsval2  15894  dvdsadd2b  15943  dvdsmod  15966  oexpneg  15982  sadass  16106  gcdass  16183  rplpwr  16195  lcmass  16247  coprmdvds2  16287  rpmulgcd2  16289  rpdvds  16293  coprmprod  16294  cncongr2  16301  rpexp  16355  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  coprimeprodsq2  16438  pythagtriplem3  16447  pythagtriplem4  16448  pcdvdsb  16498  vdwnnlem1  16624  0ram  16649  ramz2  16653  ramub1lem1  16655  mremre  17230  mrieqv2d  17265  lubss  18146  lubun  18148  clatleglb  18151  clatglbss  18152  mrelatglb  18193  isnsgrp  18294  issubmnd  18327  gsumccatOLD  18394  gsumccat  18395  frmdss2  18417  submefmnd  18449  nmzsubg  18708  ghmnsgima  18773  gsmsymgreqlem1  18953  psgnunilem4  19020  odmodnn0  19063  odnncl  19068  odmod  19069  oddvds  19070  odeq  19073  odmulgid  19076  odmulgeq  19079  odbezout  19080  odf1o1  19092  odf1o2  19093  odngen  19097  gexdvdsi  19103  pgpfi1  19115  odcau  19124  subgslw  19136  fislw  19145  lsmless1x  19164  lsmless2x  19165  lsmsubm  19173  lsmmod  19196  lsmmod2  19197  efgsfo  19260  odadd1  19364  odadd2  19365  odadd  19366  lsmcomx  19372  prdscmnd  19377  gsumconst  19450  ablsimpgfindlem1  19625  srg1zr  19680  csrgbinom  19697  ring1eq0  19744  mulgass2  19755  cntzsubr  19972  isabvd  19995  rmodislmod  20106  rmodislmodOLD  20107  0lmhm  20217  lmhmvsca  20222  reslmhm2b  20231  pwssplit1  20236  pwssplit2  20237  pwssplit3  20238  lbspss  20259  lspsnat  20322  lidldvgen  20439  xrsdsreclblem  20556  cssmre  20810  obs2ss  20846  uvcresum  20910  frlmsslsp  20913  frlmup4  20918  lindff1  20937  f1lindf  20939  lsslindf  20947  islindf4  20955  issubassa  20983  evlsval2  21207  coe1subfv  21347  coe1sclmul  21363  coe1sclmul2  21365  mpomatmul  21503  mamutpos  21515  scmatscmide  21564  mavmulsolcl  21608  mulmarep1gsum2  21631  mdetdiaglem  21655  mdetdiag  21656  mdetunilem1  21669  mdetunilem3  21671  mdetunilem9  21677  maducoeval2  21697  madurid  21701  slesolinvbi  21738  cramerimplem1  21740  cramerlem1  21744  cramer  21748  cpmatel2  21770  m2cpm  21798  m2pmfzmap  21804  m2cpminvid2lem  21811  m2cpminvid2  21812  decpmatmul  21829  pmatcollpw1lem2  21832  pmatcollpw1  21833  pmatcollpw2lem  21834  pmatcollpwfi  21839  pm2mpcl  21854  mply1topmatcl  21862  mp2pm2mplem2  21864  mp2pm2mplem4  21866  mp2pm2mplem5  21867  mp2pm2mp  21868  pm2mpghmlem2  21869  pm2mpghmlem1  21870  chfacfisfcpmat  21912  topssnei  22183  cnconst2  22342  cnpresti  22347  cnprest2  22349  cnpdis  22352  cnt0  22405  cnt1  22409  cnhaus  22413  sscmp  22464  hauscmp  22466  cnconn  22481  unconn  22488  finlocfin  22579  comppfsc  22591  kgen2ss  22614  ptpjopn  22671  prdstopn  22687  ptrescn  22698  qtopss  22774  kqfvima  22789  fbssint  22897  fbasrn  22943  filuni  22944  fmss  23005  rnelfm  23012  fmufil  23018  fmco  23020  flimss2  23031  flimss1  23032  flimrest  23042  cnpflf2  23059  flfcnp  23063  supnfcls  23079  fclsss1  23081  fclsss2  23082  isfcf  23093  subgntr  23166  opnsubg  23167  cldsubg  23170  ghmcnp  23174  ustuqtop1  23301  bldisj  23459  blgt0  23460  bl2in  23461  blss2ps  23464  blss2  23465  blssps  23485  blss  23486  xmetresbl  23498  lpbl  23565  blcld  23567  stdbdmopn  23580  metcnp3  23602  metcnp  23603  metcnp2  23604  txmetcnp  23609  blval2  23624  nmoix  23799  nmoi2  23800  nmotri  23809  metdsge  23918  metdseq0  23923  iocopnst  24009  xrhmeo  24015  nmhmcn  24189  cphsqrtcl2  24255  cphsqrtcl3  24256  cssbn  24444  pjth  24508  ovoliunlem2  24572  volun  24614  mbfimaopn2  24726  iblconst  24887  limcvallem  24940  dvfval  24966  dvcnp2  24989  dvcn  24990  deg1mul3le  25186  deg1tmle  25187  dvdsq1p  25230  ig1peu  25241  ig1pdvds  25246  ply1term  25270  coeid3  25306  dgrmulc  25337  dvply1  25349  aaliou2  25405  efcvx  25513  tanord  25599  eflogeq  25662  logdivlti  25680  logccv  25723  recxpcl  25735  cxplea  25756  cxpeq  25815  ang180  25869  isosctrlem2  25874  cxp2lim  26031  amgm  26045  muval1  26187  dvdssqf  26192  mumullem2  26234  mumul  26235  bcmono  26330  lgsneg  26374  lgsdilem  26377  lgsdirprm  26384  lgsdir  26385  lgsdi  26387  lgsne0  26388  brbtwn2  27176  colinearalglem1  27177  colinearalg  27181  axcgrtr  27186  axsegconlem8  27195  axsegconlem9  27196  axsegconlem10  27197  axcontlem2  27236  axcontlem10  27244  elntg2  27256  ewlkle  27875  crctcshwlkn0lem5  28080  wwlknp  28109  wwlksnext  28159  wwlksnextproplem1  28175  wspthsnwspthsnon  28182  clwlkclwwlklem3  28266  erclwwlksym  28286  erclwwlknsym  28335  upgriseupth  28472  eucrct2eupth  28510  3cyclfrgrrn  28551  numclwwlk2lem1lem  28607  numclwwlk1lem2foa  28619  frgrregord13  28661  nvmul0or  28913  ipval2lem2  28967  lnoadd  29021  lnosub  29022  lnomul  29023  shless  29622  shlej1  29623  kbmul  30218  homco2  30240  kbass2  30380  eliccelico  31000  elicoelioo  31001  iocinioc2  31002  iocinif  31004  difioo  31005  swrdrn2  31128  swrdrn3  31129  xrge0adddir  31203  xrge0npcan  31205  isarchi2  31341  archiabl  31354  rhmdvdsr  31419  pidlnz  31473  lindssn  31475  ssmxidl  31544  pstmfval  31748  fmcncfil  31783  zrhnm  31819  qqhnm  31840  nexple  31877  volfiniune  32098  dya2iocnrect  32148  probinc  32288  cndprob01  32302  signswmnd  32436  bnj517  32765  cvmsss2  33136  cvmlift2lem10  33174  br6  33630  funsseq  33648  nolesgn2o  33801  nogesgn1o  33803  nosep1o  33811  nosep2o  33812  nosepssdm  33816  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem4  33856  noinfbnd1lem6  33858  noinfbnd2  33861  noetasuplem3  33865  noetainflem3  33869  cofsslt  34015  coinitsslt  34016  cofcutrtime  34020  cgrtriv  34231  5segofs  34235  btwnouttr2  34251  btwnxfr  34285  lineext  34305  btwnconn1lem13  34328  brsegle2  34338  nn0prpwlem  34438  lindsenlbs  35699  blbnd  35872  ismtyima  35888  rrndstprj2  35916  ghomdiv  35977  grpokerinj  35978  lsatfixedN  36950  lssat  36957  lshpkrlem4  37054  cvrcon3b  37218  atlen0  37251  atcvreq0  37255  atnle  37258  atlatmstc  37260  atlatle  37261  cvlcvr1  37280  hlsupr2  37328  hlrelat2  37344  cvrexchlem  37360  lnnat  37368  atcvrj2b  37373  3dimlem3  37402  3dim1  37408  1cvrjat  37416  llni  37449  llni2  37453  llnexatN  37462  2llnmat  37465  lplni  37473  2atnelpln  37485  llncvrlpln2  37498  2llnmj  37501  lplnexatN  37504  lplnexllnN  37505  2llnm3N  37510  lvoli  37516  lvoli3  37518  lvolnle3at  37523  islvol2aN  37533  4atlem4a  37540  4atlem4b  37541  4atlem11  37550  lplncvrlvol2  37556  2lplnmj  37563  islinei  37681  linepmap  37716  lnjatN  37721  lncvrat  37723  lncmp  37724  elpaddn0  37741  elpaddatriN  37744  elpaddat  37745  paddcom  37754  paddss2  37759  paddss12  37760  paddasslem4  37764  paddasslem9  37769  paddasslem10  37770  pmodl42N  37792  pmapjoin  37793  llnmod1i2  37801  polcon2bN  37861  pclfinclN  37891  poml4N  37894  poml6N  37896  osumcllem1N  37897  osumcllem2N  37898  osumcllem11N  37907  osumclN  37908  pmapojoinN  37909  pexmidlem2N  37912  pexmidlem3N  37913  pexmidlem4N  37914  pexmidlem6N  37916  pexmidlem7N  37917  pl42lem2N  37921  pl42lem3N  37922  pl42lem4N  37923  pl42N  37924  lhprelat3N  37981  4atex  38017  lauteq  38036  lautco  38038  ltrncoidN  38069  ltrneq2  38089  ltrnideq  38116  trlnle  38127  trlval3  38128  cdlemc  38138  cdlemd9  38147  cdlemd  38148  cdleme21j  38277  cdleme21  38278  cdleme29ex  38315  cdlemefr27cl  38344  cdlemefs27cl  38354  cdleme32d  38385  cdleme32f  38387  cdleme35h2  38398  cdleme40m  38408  cdleme17d3  38437  cdleme48fvg  38441  cdlemeg46fvcl  38447  cdlemeg46fgN  38475  cdleme48fgv  38479  cdleme50trn3  38494  cdlemb3  38547  cdlemg8  38572  cdlemg11a  38578  cdlemg15a  38596  cdlemg15  38597  cdlemg16  38598  cdlemg16z  38600  cdlemg17dN  38604  cdlemg24  38629  cdlemg37  38630  cdlemg29  38646  cdlemg33b  38648  cdlemg38  38656  cdlemg40  38658  trlco  38668  cdlemg44b  38673  ltrncom  38679  trljco  38681  tendococl  38713  tendoplcl  38722  tendoplcom  38723  cdlemj2  38763  tendoid0  38766  tendo1ne0  38769  cdlemk25-3  38845  cdlemk36  38854  cdlemkid4  38875  cdlemk19x  38884  cdlemk53  38898  cdlemk56  38912  cdleml5N  38921  tendospcanN  38964  cdlemm10N  39059  dihord6apre  39197  dihord  39205  dihmeetlem1N  39231  dihglblem2N  39235  dihmeetlem2N  39240  dihmeetbN  39244  dihmeetlem5  39249  dihmeetlem6  39250  dihmeetlem7N  39251  dihmeetlem10N  39257  dihmeetlem12N  39259  dihmeetlem16N  39263  dihmeetlem17N  39264  dihmeetlem18N  39265  dihmeetALTN  39268  dihlspsnssN  39273  dvh3dim2  39389  dvh3dim3N  39390  lcfrlem16  39499  mapdrvallem2  39586  mapdh8ad  39720  hgmapvvlem3  39866  sticksstones1  40030  sticksstones2  40031  resubcan2  40292  diophrw  40497  eldioph2lem1  40498  diophrex  40513  rencldnfi  40559  pellexlem2  40568  pellqrexplicit  40615  infmrgelbi  40616  pellfundglb  40623  pellfund14gap  40625  rmxycomplete  40655  congadd  40704  acongeq  40721  jm2.19  40731  jm2.23  40734  jm2.20nn  40735  jm2.27  40746  jm3.1  40758  lnmepi  40826  lmhmlnmsplit  40828  hbtlem2  40865  dgraa0p  40890  idomrootle  40936  proot1hash  40941  iocunico  40958  iocinico  40959  relexpxpmin  41214  ntrclsk3  41569  grur1cld  41739  ismnu  41768  grumnudlem  41792  ismnushort  41808  rfcnnnub  42468  uzwo4  42490  wessf1ornlem  42611  supxrge  42767  infleinflem2  42800  iccintsng  42951  climsuse  43039  lptre2pt  43071  limcleqr  43075  0ellimcdiv  43080  fnlimfvre  43105  dvnprodlem1  43377  volioc  43403  stoweidlem17  43448  stoweidlem19  43450  stoweidlem20  43451  stoweidlem22  43453  stoweidlem28  43459  stoweidlem34  43465  stoweidlem44  43475  stoweidlem60  43491  wallispilem3  43498  fourierdlem42  43580  fourierdlem48  43585  fourierdlem51  43588  fourierdlem54  43591  fourierdlem74  43611  fourierdlem77  43614  fourierdlem87  43624  fourierdlem97  43634  ioorrnopnlem  43735  ovnsubaddlem2  43999  smfinflem  44237  eluzge0nn0  44692  fzopredsuc  44703  fzoopth  44707  imasetpreimafvbijlemfv  44742  lighneallem4  44950  oexpnegALTV  45017  oexpnegnz  45018  tgblthelfgott  45155  rmsupp0  45592  rmsuppss  45594  lincresunit3lem3  45703  lincresunit3lem2  45709  lindssnlvec  45715  fdivmptf  45775  refdivmptf  45776  elbigolo1  45791  rrx2linest  45976  itsclc0lem1  45990  itsclc0lem2  45991  itsclc0yqsollem1  45996  itsclc0b  46006