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  7292  weniso  7364  ofmpteq  7716  tfisi  7870  mposn  8114  fprlem1  8319  smogt  8376  smocdmdom  8377  omeulem1  8591  nnmord  8642  nnmword  8643  naddasslem1  8705  naddasslem2  8706  difsnen  9079  enfixsn  9106  mapunen  9166  ac6sfi  9276  ordiso2  9510  wemaplem2  9542  wemapso2lem  9547  en2eqpr  10087  acndom  10131  infmap2  10296  cflim2  10342  cfsmolem  10349  coftr  10352  fin23lem26  10404  isf32lem9  10440  fin1a2lem9  10487  fin1a2lem10  10488  gchdomtri  10715  canth4  10733  gchpwdom  10756  gruima  10888  grudomon  10903  prn0  11075  distrlem4pr  11112  prlem934  11119  addcan  11495  addcan2  11496  divmulass  11998  divmulasscom  11999  ltmul1a  12167  supmul1  12287  uzsupss  13068  xaddass  13380  xleadd1a  13384  xlesubadd  13394  xmulass  13418  xlemul2a  13420  xadddilem  13425  xadddi  13426  ixxdisj  13492  ixxun  13493  ixxlb  13499  icoshftf1o  13606  icodisj  13608  ioounsn  13609  lincmb01cmp  13627  iccf1o  13628  elfz1b  13728  ssfzoulel  13896  fzoopth  13898  modmuladd  14057  modaddmulmod  14082  ltexp2a  14310  leexp2  14315  ltexp2r  14317  exple1  14321  expnlbnd2  14379  mulsubdivbinom2  14407  fun2dmnop0  14650  ccatass  14735  swrdrn3  14803  ccatopth  14866  pfxccatin12lem2a  14877  repswpfx  14937  repswccat  14938  cshwidxmodr  14956  2cshw  14965  repsco  14992  s2f1o  15068  limsupgle  15645  limsupgre  15649  addcn2  15762  mulcn2  15764  binomrisefac  16209  dvdsval2  16426  dvdsadd2b  16477  dvdsmod  16500  oexpneg  16516  sadass  16642  gcdass  16721  rplpwr  16733  lcmass  16790  coprmdvds2  16830  rpmulgcd2  16832  rpdvds  16836  coprmprod  16837  cncongr2  16844  rpexp  16899  prmdiveq  16964  hashgcdlem  16966  odzdvds  16974  coprimeprodsq2  16988  pythagtriplem3  16997  pythagtriplem4  16998  pcdvdsb  17048  vdwnnlem1  17174  0ram  17199  ramz2  17203  ramub1lem1  17205  mremre  17775  mrieqv2d  17814  lubss  18688  lubun  18690  clatleglb  18693  clatglbss  18694  mrelatglb  18735  isnsgrp  18913  issubmnd  18954  gsumccat  19038  frmdss2  19060  submefmnd  19092  nmzsubg  19376  ghmnsgima  19455  gsmsymgreqlem1  19645  psgnunilem4  19712  odmodnn0  19755  odnncl  19760  odmod  19761  oddvds  19762  odeq  19765  odmulgid  19769  odmulgeq  19772  odbezout  19773  odf1o1  19787  odf1o2  19788  odngen  19792  gexdvdsi  19798  pgpfi1  19810  odcau  19819  subgslw  19831  fislw  19840  lsmless1x  19859  lsmless2x  19860  lsmsubm  19868  lsmmod  19890  lsmmod2  19891  efgsfo  19954  odadd1  20063  odadd2  20064  odadd  20065  lsmcomx  20071  prdscmnd  20076  gsumconst  20149  ablsimpgfindlem1  20324  csrgbinom  20459  ring1eq0  20530  mulgass2  20541  rngisom1  20697  rhmdvdsr  20759  cntzsubrng  20820  cntzsubr  20859  isdrng3lem2  21007  isabvd  21070  rmodislmod  21206  0lmhm  21316  lmhmvsca  21321  reslmhm2b  21330  pwssplit1  21335  pwssplit2  21336  pwssplit3  21337  lbspss  21358  lspsnat  21424  pidlnz  21529  lidldvgen  21659  xrsdsreclblem  21720  cssmre  22000  obs2ss  22036  uvcresum  22100  frlmsslsp  22103  frlmup4  22108  lindff1  22127  f1lindf  22129  lsslindf  22137  islindf4  22145  lindsenlbs  22158  issubassa  22176  evlsval2  22397  coe1subfv  22586  coe1sclmul  22602  coe1sclmul2  22604  mpomatmul  22762  mamutpos  22774  scmatscmide  22823  mavmulsolcl  22867  mulmarep1gsum2  22890  mdetdiaglem  22914  mdetdiag  22915  mdetunilem1  22928  mdetunilem3  22930  mdetunilem9  22936  maducoeval2  22956  madurid  22960  slesolinvbi  23000  cramerimplem1  23002  cramerlem1  23006  cramer  23010  cpmatel2  23032  m2cpm  23060  m2pmfzmap  23066  m2cpminvid2lem  23073  m2cpminvid2  23074  decpmatmul  23091  pmatcollpw1lem2  23094  pmatcollpw1  23095  pmatcollpw2lem  23096  pmatcollpwfi  23101  pm2mpcl  23116  mply1topmatcl  23124  mp2pm2mplem2  23126  mp2pm2mplem4  23128  mp2pm2mplem5  23129  mp2pm2mp  23130  pm2mpghmlem2  23131  pm2mpghmlem1  23132  chfacfisfcpmat  23174  topssnei  23443  cnconst2  23602  cnpresti  23607  cnprest2  23609  cnpdis  23612  cnt0  23665  cnt1  23669  cnhaus  23673  sscmp  23724  hauscmp  23726  cnconn  23741  unconn  23748  finlocfin  23840  comppfsc  23852  kgen2ss  23875  ptpjopn  23932  prdstopn  23948  ptrescn  23959  qtopss  24035  kqfvima  24050  fbssint  24158  fbasrn  24204  filuni  24205  fmss  24266  rnelfm  24273  fmufil  24279  fmco  24281  flimss2  24292  flimss1  24293  flimrest  24303  cnpflf2  24320  flfcnp  24324  supnfcls  24340  fclsss1  24342  fclsss2  24343  isfcf  24354  subgntr  24427  opnsubg  24428  cldsubg  24431  ghmcnp  24435  ustuqtop1  24561  bldisj  24718  blgt0  24719  bl2in  24720  blss2ps  24723  blss2  24724  blssps  24744  blss  24745  xmetresbl  24757  lpbl  24823  blcld  24825  stdbdmopn  24838  metcnp3  24860  metcnp  24861  metcnp2  24862  txmetcnp  24867  blval2  24882  nmoix  25049  nmoi2  25050  nmotri  25059  metdsge  25170  metdseq0  25175  iocopnst  25262  xrhmeo  25268  nmhmcn  25442  cphsqrtcl2  25508  cphsqrtcl3  25509  cssbn  25697  pjth  25761  ovoliunlem2  25825  volun  25867  mbfimaopn2  25979  iblconst  26139  limcvallem  26192  dvfval  26218  dvcnp2  26241  dvcn  26242  deg1mul3le  26436  deg1tmle  26437  dvdsq1p  26482  idomrootle  26492  ig1peu  26494  ig1pdvds  26499  ply1term  26523  coeid3  26560  dgrmulc  26591  dvply1  26606  aaliou2  26668  efcvx  26777  tanord  26867  eflogeq  26931  logdivlti  26949  logccv  26992  recxpcl  27004  cxplea  27025  cxpeq  27086  ang180  27143  isosctrlem2  27148  cxp2lim  27305  amgm  27319  muval1  27461  dvdssqf  27466  mumullem2  27508  mumul  27509  bcmono  27605  lgsneg  27649  lgsdilem  27652  lgsdirprm  27659  lgsdir  27660  lgsdi  27662  lgsne0  27663  nolesgn2o  28029  nogesgn1o  28031  nosep1o  28039  nosep2o  28040  nosepssdm  28044  nosupres  28065  nosupbnd1lem1  28066  nosupbnd1lem4  28069  nosupbnd1lem5  28070  nosupbnd1lem6  28071  noinfres  28080  noinfbnd1lem1  28081  noinfbnd1lem4  28084  noinfbnd1lem6  28086  noinfbnd2  28089  noetasuplem3  28093  noetainflem3  28097  leslss  28296  cofslts  28305  coinitslts  28306  cofcutrtime  28314  addsass  28392  addsdi  28542  mulsass  28553  ltmuls2  28558  divmulsw  28580  bdayfinbndlem1  28854  z12bdaylem  28871  brbtwn2  29484  colinearalglem1  29485  colinearalg  29489  axcgrtr  29494  axsegconlem8  29503  axsegconlem9  29504  axsegconlem10  29505  axcontlem2  29544  axcontlem10  29552  elntg2  29564  ewlkle  30187  crctcshwlkn0lem5  30404  wwlknp  30433  wwlksnext  30483  wwlksnextproplem1  30499  wspthsnwspthsnon  30506  clwlkclwwlklem3  30593  erclwwlksym  30613  erclwwlknsym  30662  upgriseupth  30809  eucrct2eupth  30847  3cyclfrgrrn  30888  numclwwlk2lem1lem  30944  numclwwlk1lem2foa  30956  frgrregord13  30998  nvmul0or  31253  ipval2lem2  31307  lnoadd  31361  lnosub  31362  lnomul  31363  shless  31962  shlej1  31963  kbmul  32558  homco2  32580  kbass2  32720  eliccelico  33412  elicoelioo  33413  iocinioc2  33414  iocinif  33416  difioo  33417  nexple  33467  swrdrn2  33560  xrge0adddir  33622  xrge0npcan  33624  isarchi2  33789  archiabl  33802  lindssn  33976  ssmxidl  34042  pstmfval  34571  fmcncfil  34606  zrhnm  34642  qqhnm  34665  volfiniune  34906  dya2iocnrect  34956  probinc  35096  cndprob01  35110  signswmnd  35229  bnj517  35558  cvmsss2  36108  cvmlift2lem10  36146  br6  36597  funsseq  36608  cgrtriv  36842  5segofs  36846  btwnouttr2  36862  btwnxfr  36896  lineext  36916  btwnconn1lem13  36939  brsegle2  36949  nmulss1  37038  ltnmul  37040  nmulle  37041  ltnadd  37042  naddle  37043  nadddi  37048  nn0prpwlem  37185  weiunpo  37328  weiunso  37329  weiunfr  37330  weiunse  37331  axtcond  37341  blbnd  38797  ismtyima  38813  rrndstprj2  38841  ghomdiv  38902  grpokerinj  38903  lsatfixedN  40142  lssat  40149  lshpkrlem4  40246  cvrcon3b  40410  atlen0  40443  atcvreq0  40447  atnle  40450  atlatmstc  40452  atlatle  40453  cvlcvr1  40472  hlsupr2  40520  hlrelat2  40536  cvrexchlem  40552  lnnat  40560  atcvrj2b  40565  3dimlem3  40594  3dim1  40600  1cvrjat  40608  llni  40641  llni2  40645  llnexatN  40654  2llnmat  40657  lplni  40665  2atnelpln  40677  llncvrlpln2  40690  2llnmj  40693  lplnexatN  40696  lplnexllnN  40697  2llnm3N  40702  lvoli  40708  lvoli3  40710  lvolnle3at  40715  islvol2aN  40725  4atlem4a  40732  4atlem4b  40733  4atlem11  40742  lplncvrlvol2  40748  2lplnmj  40755  islinei  40873  linepmap  40908  lnjatN  40913  lncvrat  40915  lncmp  40916  elpaddn0  40933  elpaddatriN  40936  elpaddat  40937  paddcom  40946  paddss2  40951  paddss12  40952  paddasslem4  40956  paddasslem9  40961  paddasslem10  40962  pmodl42N  40984  pmapjoin  40985  llnmod1i2  40993  polcon2bN  41053  pclfinclN  41083  poml4N  41086  poml6N  41088  osumcllem1N  41089  osumcllem2N  41090  osumcllem11N  41099  osumclN  41100  pmapojoinN  41101  pexmidlem2N  41104  pexmidlem3N  41105  pexmidlem4N  41106  pexmidlem6N  41108  pexmidlem7N  41109  pl42lem2N  41113  pl42lem3N  41114  pl42lem4N  41115  pl42N  41116  lhprelat3N  41173  4atex  41209  lauteq  41228  lautco  41230  ltrncoidN  41261  ltrneq2  41281  ltrnideq  41308  trlnle  41319  trlval3  41320  cdlemc  41330  cdlemd9  41339  cdlemd  41340  cdleme21j  41469  cdleme21  41470  cdleme29ex  41507  cdlemefr27cl  41536  cdlemefs27cl  41546  cdleme32d  41577  cdleme32f  41579  cdleme35h2  41590  cdleme40m  41600  cdleme17d3  41629  cdleme48fvg  41633  cdlemeg46fvcl  41639  cdlemeg46fgN  41667  cdleme48fgv  41671  cdleme50trn3  41686  cdlemb3  41739  cdlemg8  41764  cdlemg11a  41770  cdlemg15a  41788  cdlemg15  41789  cdlemg16  41790  cdlemg16z  41792  cdlemg17dN  41796  cdlemg24  41821  cdlemg37  41822  cdlemg29  41838  cdlemg33b  41840  cdlemg38  41848  cdlemg40  41850  trlco  41860  cdlemg44b  41865  ltrncom  41871  trljco  41873  tendococl  41905  tendoplcl  41914  tendoplcom  41915  cdlemj2  41955  tendoid0  41958  tendo1ne0  41961  cdlemk25-3  42037  cdlemk36  42046  cdlemkid4  42067  cdlemk19x  42076  cdlemk53  42090  cdlemk56  42104  cdleml5N  42113  tendospcanN  42156  cdlemm10N  42251  dihord6apre  42389  dihord  42397  dihmeetlem1N  42423  dihglblem2N  42427  dihmeetlem2N  42432  dihmeetbN  42436  dihmeetlem5  42441  dihmeetlem6  42442  dihmeetlem7N  42443  dihmeetlem10N  42449  dihmeetlem12N  42451  dihmeetlem16N  42455  dihmeetlem17N  42456  dihmeetlem18N  42457  dihmeetALTN  42460  dihlspsnssN  42465  dvh3dim2  42581  dvh3dim3N  42582  lcfrlem16  42691  mapdrvallem2  42778  mapdh8ad  42912  hgmapvvlem3  43058  sticksstones1  43272  sticksstones2  43273  aks6d1c6isolem1  43300  resubcan2  43515  diophrw  43846  eldioph2lem1  43847  diophrex  43862  rencldnfi  43904  pellexlem2  43913  pellqrexplicit  43960  infmrgelbi  43961  pellfundglb  43968  pellfund14gap  43970  rmxycomplete  44000  congadd  44049  acongeq  44066  jm2.19  44076  jm2.23  44079  jm2.20nn  44080  jm2.27  44091  jm3.1  44103  lnmepi  44163  lmhmlnmsplit  44165  hbtlem2  44202  dgraa0p  44227  proot1hash  44273  iocunico  44289  iocinico  44290  oasubex  44364  cantnf2  44403  onmcl  44409  omcl2  44411  nadd2rabex  44464  nadd1rabtr  44466  nadd1rabex  44468  fzunt  44532  relexpxpmin  44793  ntrclsk3  45146  grur1cld  45306  ismnu  45321  grumnudlem  45345  ismnushort  45361  rfcnnnub  46129  uzwo4  46146  wessf1ornlem  46276  supxrge  46426  infleinflem2  46458  iccintsng  46611  climsuse  46696  lptre2pt  46726  limcleqr  46730  0ellimcdiv  46735  fnlimfvre  46760  dvnprodlem1  47032  volioc  47058  stoweidlem17  47103  stoweidlem19  47105  stoweidlem20  47106  stoweidlem22  47108  stoweidlem28  47114  stoweidlem34  47120  stoweidlem44  47130  stoweidlem60  47146  wallispilem3  47153  fourierdlem42  47235  fourierdlem48  47240  fourierdlem51  47243  fourierdlem54  47246  fourierdlem74  47266  fourierdlem77  47269  fourierdlem87  47279  fourierdlem97  47289  ioorrnopnlem  47390  ovnsubaddlem2  47657  smfinflem  47903  fsupdm  47928  finfdm  47932  eluzge0nn0  48458  fzopredsuc  48470  imasetpreimafvbijlemfv  48560  lighneallem4  48771  oexpnegALTV  48851  oexpnegnz  48852  tgblthelfgott  48989  clnbgrgrim  49108  isubgr3stgrlem3  49142  rmsupp0  49556  rmsuppss  49558  lincresunit3lem3  49662  lincresunit3lem2  49668  lindssnlvec  49674  fdivmptf  49729  refdivmptf  49730  elbigolo1  49745  rrx2linest  49930  itsclc0lem1  49944  itsclc0lem2  49945  itsclc0yqsollem1  49950  itsclc0b  49960  setc1onsubc  50786