Theorem simpl2 1237

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  simpll2OLD  1265  simprl2OLD  1277  simpl12  1324  simpl22  1330  simpl32  1336  simp1l2  1359  simp2l2  1365  simp3l2  1371  3anandirs  1589  rspc3ev  3519  f1prex  6759  weniso  6824  ofmpteq  7142  tfisi  7284  mpt2sn  7498  smogt  7696  smorndom  7697  omeulem1  7895  nnmord  7945  nnmword  7946  difsnen  8277  enfixsn  8304  mapunen  8364  ac6sfi  8439  ordiso2  8655  wemaplem2  8687  wemapso  8691  wemapso2lem  8692  en2eqpr  9109  acndom  9153  infmap2  9321  cflim2  9366  cfsmolem  9373  coftr  9376  fin23lem26  9428  isf32lem9  9464  fin1a2lem9  9511  fin1a2lem10  9512  ac6num  9582  gchdomtri  9732  canth4  9750  gchpwdom  9773  gruima  9905  grudomon  9920  prn0  10092  distrlem4pr  10129  prlem934  10136  addcan  10501  addcan2  10502  divmulass  10989  divmulasscom  10990  ltmul1a  11153  supmul1  11273  uzsupss  11995  xaddass  12293  xleadd1a  12297  xlesubadd  12307  xmulass  12331  xlemul2a  12333  xadddilem  12338  xadddi  12339  ixxdisj  12404  ixxun  12405  ixxlb  12411  icoshftf1o  12512  icodisj  12514  ioounsn  12515  lincmb01cmp  12534  iccf1o  12535  elfz1b  12628  ssfzoulel  12782  modmuladd  12932  modaddmulmod  12957  ltexp2a  13131  leexp2  13134  ltexp2r  13136  exple1  13139  expnlbnd2  13214  mulsubdivbinom2  13265  fun2dmnop0  13489  ccatass  13581  ccatopth  13690  swrdccatin12lem2a  13705  repswccat  13752  cshwidxmodr  13770  2cshw  13779  repsco  13805  s2f1o  13881  limsupgle  14427  limsupgre  14431  addcn2  14543  mulcn2  14545  binomrisefac  14989  dvdsval2  15202  dvdsadd2b  15247  dvdsmod  15269  oexpneg  15285  sadass  15408  gcdass  15479  rplpwr  15491  rppwr  15492  lcmass  15542  coprmdvds2  15582  rpmulgcd2  15584  rpdvds  15588  coprmprod  15589  cncongr2  15596  rpexp  15645  prmdiveq  15704  hashgcdlem  15706  odzdvds  15713  coprimeprodsq2  15727  pythagtriplem3  15736  pythagtriplem4  15737  pcdvdsb  15786  vdwnnlem1  15912  0ram  15937  ramz2  15941  ramub1lem1  15943  mremre  16465  mrieqv2d  16500  lubss  17322  lubun  17324  clatleglb  17327  clatglbss  17328  mrelatglb  17385  isnsgrp  17489  issubmnd  17519  gsumccat  17579  frmdss2  17601  nmzsubg  17833  ghmnsgima  17882  gsmsymgreqlem1  18047  psgnunilem4  18114  odmodnn0  18156  odnncl  18161  odmod  18162  oddvds  18163  odeq  18166  odmulgid  18168  odmulgeq  18171  odbezout  18172  odf1o1  18184  odf1o2  18185  odngen  18189  gexdvdsi  18195  pgpfi1  18207  odcau  18216  subgslw  18228  fislw  18237  lsmless1x  18256  lsmless2x  18257  lsmsubm  18265  lsmmod  18285  lsmmod2  18286  efgsfo  18349  odadd1  18448  odadd2  18449  odadd  18450  lsmcomx  18456  prdscmnd  18461  gsumconst  18531  srg1zr  18727  csrgbinom  18744  ring1eq0  18788  mulgass2  18799  cntzsubr  19012  isabvd  19020  rmodislmod  19131  0lmhm  19243  lmhmvsca  19248  reslmhm2b  19257  pwssplit1  19262  pwssplit2  19263  pwssplit3  19264  lbspss  19285  lspsnat  19349  lidldvgen  19460  issubassa  19529  evlsval2  19724  coe1subfv  19840  coe1sclmul  19856  coe1sclmul2  19858  xrsdsreclblem  19996  cssmre  20244  obs2ss  20280  uvcresum  20339  frlmsslsp  20342  frlmup4  20347  lindff1  20366  f1lindf  20368  lsslindf  20376  islindf4  20384  mpt2matmul  20460  mamutpos  20472  scmatscmide  20521  mavmulsolcl  20565  mulmarep1gsum2  20588  mdetdiaglem  20612  mdetdiag  20613  mdetunilem1  20626  mdetunilem3  20628  mdetunilem9  20634  maducoeval2  20654  madurid  20658  slesolinvbi  20696  cramerimplem1  20698  cramerimplem1OLD  20699  cramerlem1  20703  cramer  20707  cpmatel2  20728  m2cpm  20756  m2pmfzmap  20762  m2cpminvid2lem  20769  m2cpminvid2  20770  decpmatmul  20787  pmatcollpw1lem2  20790  pmatcollpw1  20791  pmatcollpw2lem  20792  pmatcollpwfi  20797  pm2mpcl  20812  mply1topmatcl  20820  mp2pm2mplem2  20822  mp2pm2mplem4  20824  mp2pm2mplem5  20825  mp2pm2mp  20826  pm2mpghmlem2  20827  pm2mpghmlem1  20828  chfacfisfcpmat  20870  topssnei  21139  cnconst2  21298  cnpresti  21303  cnprest2  21305  cnpdis  21308  cnt0  21361  cnt1  21365  cnhaus  21369  sscmp  21419  hauscmp  21421  cnconn  21436  unconn  21443  finlocfin  21534  comppfsc  21546  kgen2ss  21569  ptpjopn  21626  prdstopn  21642  ptrescn  21653  qtopss  21729  kqfvima  21744  fbssint  21852  fbasrn  21898  filuni  21899  fmss  21960  rnelfm  21967  fmufil  21973  fmco  21975  flimss2  21986  flimss1  21987  flimrest  21997  cnpflf2  22014  flfcnp  22018  supnfcls  22034  fclsss1  22036  fclsss2  22037  isfcf  22048  subgntr  22120  opnsubg  22121  cldsubg  22124  ghmcnp  22128  ustuqtop1  22255  bldisj  22413  blgt0  22414  bl2in  22415  blss2ps  22418  blss2  22419  blssps  22439  blss  22440  xmetresbl  22452  lpbl  22518  blcld  22520  stdbdmopn  22533  metcnp3  22555  metcnp  22556  metcnp2  22557  txmetcnp  22562  blval2  22577  nmoix  22743  nmoi2  22744  nmotri  22753  metdsge  22862  metdseq0  22867  iocopnst  22949  xrhmeo  22955  nmhmcn  23129  cphsqrtcl2  23195  cphsqrtcl3  23196  pjth  23421  ovoliunlem2  23483  volun  23525  mbfimaopn2  23637  iblconst  23797  limcvallem  23848  dvfval  23874  dvcnp2  23896  dvcn  23897  deg1mul3le  24089  deg1tmle  24090  dvdsq1p  24133  ig1peu  24144  ig1pdvds  24149  ply1term  24173  coeid3  24209  dgrmulc  24240  dvply1  24252  aaliou2  24308  efcvx  24416  tanord  24498  eflogeq  24561  logdivlti  24579  logccv  24622  recxpcl  24634  cxplea  24655  cxpeq  24711  ang180  24757  isosctrlem2  24762  cxp2lim  24916  amgm  24930  muval1  25072  dvdssqf  25077  mumullem2  25119  mumul  25120  bcmono  25215  lgsneg  25259  lgsdilem  25262  lgsdirprm  25269  lgsdir  25270  lgsdi  25272  lgsne0  25273  brbtwn2  25998  colinearalglem1  25999  colinearalg  26003  axcgrtr  26008  axsegconlem8  26017  axsegconlem9  26018  axsegconlem10  26019  axcontlem2  26058  axcontlem10  26066  ewlkle  26728  edginwlkOLD  26758  crctcshwlkn0lem5  26934  wwlknp  26963  wwlksnext  27029  wwlksnextproplem1  27046  wspthsnwspthsnon  27053  wspthsnwspthsnonOLD  27055  clwlkclwwlklem3  27143  erclwwlksym  27163  erclwwlknsym  27220  clwwlknonex2lem2  27276  upgriseupth  27379  eucrct2eupth  27417  3cyclfrgrrn  27460  numclwwlk2lem1lem  27517  numclwwlk1lem2foa  27532  frgrregord13  27583  nvmul0or  27832  ipval2lem2  27886  lnoadd  27940  lnosub  27941  lnomul  27942  shless  28545  shlej1  28546  kbmul  29141  homco2  29163  kbass2  29303  eliccelico  29865  elicoelioo  29866  iocinioc2  29867  iocinif  29869  difioo  29870  xrge0adddir  30016  xrge0npcan  30018  isarchi2  30063  archiabl  30076  rhmdvdsr  30142  pstmfval  30263  fmcncfil  30301  zrhnm  30337  qqhnm  30358  nexple  30395  volfiniune  30617  dya2iocnrect  30667  probinc  30807  cndprob01  30821  signswmnd  30958  bnj517  31276  cvmsss2  31577  cvmlift2lem10  31615  br6  31967  funsseq  31986  nolesgn2o  32143  nosep1o  32151  nosepssdm  32155  nosupres  32172  nosupbnd1lem1  32173  nosupbnd1lem4  32176  nosupbnd1lem5  32177  nosupbnd1lem6  32178  noetalem2  32183  cgrtriv  32428  5segofs  32432  btwnouttr2  32448  btwnxfr  32482  lineext  32502  btwnconn1lem13  32525  brsegle2  32535  nn0prpwlem  32636  lindsenlbs  33715  blbnd  33895  ismtyima  33911  rrndstprj2  33939  ghomdiv  34000  grpokerinj  34001  lsatfixedN  34787  lssat  34794  lshpkrlem4  34891  cvrcon3b  35055  atlen0  35088  atcvreq0  35092  atnle  35095  atlatmstc  35097  atlatle  35098  cvlcvr1  35117  hlsupr2  35165  hlrelat2  35181  cvrexchlem  35197  lnnat  35205  atcvrj2b  35210  3dimlem3  35239  3dim1  35245  1cvrjat  35253  llni  35286  llni2  35290  llnexatN  35299  2llnmat  35302  lplni  35310  2atnelpln  35322  llncvrlpln2  35335  2llnmj  35338  lplnexatN  35341  lplnexllnN  35342  2llnm3N  35347  lvoli  35353  lvoli3  35355  lvolnle3at  35360  islvol2aN  35370  4atlem4a  35377  4atlem4b  35378  4atlem11  35387  lplncvrlvol2  35393  2lplnmj  35400  islinei  35518  linepmap  35553  lnjatN  35558  lncvrat  35560  lncmp  35561  elpaddn0  35578  elpaddatriN  35581  elpaddat  35582  paddcom  35591  paddss2  35596  paddss12  35597  paddasslem4  35601  paddasslem9  35606  paddasslem10  35607  pmodl42N  35629  pmapjoin  35630  llnmod1i2  35638  polcon2bN  35698  pclfinclN  35728  poml4N  35731  poml6N  35733  osumcllem1N  35734  osumcllem2N  35735  osumcllem11N  35744  osumclN  35745  pmapojoinN  35746  pexmidlem2N  35749  pexmidlem3N  35750  pexmidlem4N  35751  pexmidlem6N  35753  pexmidlem7N  35754  pl42lem2N  35758  pl42lem3N  35759  pl42lem4N  35760  pl42N  35761  lhprelat3N  35818  4atex  35854  lauteq  35873  lautco  35875  ltrncoidN  35906  ltrneq2  35926  ltrnideq  35953  trlnle  35964  trlval3  35965  cdlemc  35975  cdlemd9  35984  cdlemd  35985  cdleme21j  36114  cdleme21  36115  cdleme29ex  36152  cdlemefr27cl  36181  cdlemefs27cl  36191  cdleme32d  36222  cdleme32f  36224  cdleme35h2  36235  cdleme40m  36245  cdleme17d3  36274  cdleme48fvg  36278  cdlemeg46fvcl  36284  cdlemeg46fgN  36312  cdleme48fgv  36316  cdleme50trn3  36331  cdlemb3  36384  cdlemg8  36409  cdlemg11a  36415  cdlemg15a  36433  cdlemg15  36434  cdlemg16  36435  cdlemg16z  36437  cdlemg17dN  36441  cdlemg24  36466  cdlemg37  36467  cdlemg29  36483  cdlemg33b  36485  cdlemg38  36493  cdlemg40  36495  trlco  36505  cdlemg44b  36510  ltrncom  36516  trljco  36518  tendococl  36550  tendoplcl  36559  tendoplcom  36560  cdlemj2  36600  tendoid0  36603  tendo1ne0  36606  cdlemk25-3  36682  cdlemk36  36691  cdlemkid4  36712  cdlemk19x  36721  cdlemk53  36735  cdlemk56  36749  cdleml5N  36758  tendospcanN  36801  cdlemm10N  36896  dihord6apre  37034  dihord  37042  dihmeetlem1N  37068  dihglblem2N  37072  dihmeetlem2N  37077  dihmeetbN  37081  dihmeetlem5  37086  dihmeetlem6  37087  dihmeetlem7N  37088  dihmeetlem10N  37094  dihmeetlem12N  37096  dihmeetlem16N  37100  dihmeetlem17N  37101  dihmeetlem18N  37102  dihmeetALTN  37105  dihlspsnssN  37110  dvh3dim2  37226  dvh3dim3N  37227  lcfrlem16  37336  mapdrvallem2  37423  mapdh8ad  37557  hgmapvvlem3  37703  diophrw  37821  eldioph2lem1  37822  diophrex  37838  rencldnfi  37884  pellexlem2  37893  pellqrexplicit  37940  infmrgelbi  37941  pellfundglb  37948  pellfund14gap  37950  rmxycomplete  37980  congadd  38031  acongeq  38048  jm2.19  38058  jm2.23  38061  jm2.20nn  38062  jm2.27  38073  jm3.1  38085  lnmepi  38153  lmhmlnmsplit  38155  hbtlem2  38192  dgraa0p  38217  idomrootle  38271  proot1hash  38276  iocunico  38293  iocinico  38294  relexpxpmin  38506  ntrclsk3  38865  rfcnnnub  39686  uzwo4  39711  supxrge  40031  infleinflem2  40064  iccintsng  40227  climsuse  40317  lptre2pt  40349  limcleqr  40353  0ellimcdiv  40358  fnlimfvre  40383  dvnprodlem1  40638  volioc  40664  stoweidlem17  40710  stoweidlem19  40712  stoweidlem20  40713  stoweidlem22  40715  stoweidlem28  40721  stoweidlem34  40727  stoweidlem44  40737  stoweidlem60  40753  wallispilem3  40760  fourierdlem42  40842  fourierdlem48  40847  fourierdlem51  40850  fourierdlem54  40853  fourierdlem74  40873  fourierdlem77  40876  fourierdlem87  40886  fourierdlem97  40896  ioorrnopnlem  41000  ovnsubaddlem2  41264  smfinflem  41502  eluzge0nn0  41894  fzopredsuc  41905  fzoopth  41909  repswpfx  42008  lighneallem4  42099  oexpnegALTV  42160  oexpnegnz  42161  tgblthelfgott  42275  rmsupp0  42714  rmsuppss  42716  lincresunit3lem3  42828  lincresunit3lem2  42834  lindssnlvec  42840  fdivmptf  42900  refdivmptf  42901  elbigolo1  42916