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  8318  smogt  8375  smocdmdom  8376  omeulem1  8590  nnmord  8641  nnmword  8642  naddasslem1  8704  naddasslem2  8705  difsnen  9078  enfixsn  9105  mapunen  9165  ac6sfi  9275  ordiso2  9509  wemaplem2  9541  wemapso2lem  9546  en2eqpr  10086  acndom  10130  infmap2  10295  cflim2  10341  cfsmolem  10348  coftr  10351  fin23lem26  10403  isf32lem9  10439  fin1a2lem9  10486  fin1a2lem10  10487  gchdomtri  10714  canth4  10732  gchpwdom  10755  gruima  10887  grudomon  10902  prn0  11074  distrlem4pr  11111  prlem934  11118  addcan  11494  addcan2  11495  divmulass  11997  divmulasscom  11998  ltmul1a  12166  supmul1  12286  uzsupss  13067  xaddass  13379  xleadd1a  13383  xlesubadd  13393  xmulass  13417  xlemul2a  13419  xadddilem  13424  xadddi  13425  ixxdisj  13491  ixxun  13492  ixxlb  13498  icoshftf1o  13605  icodisj  13607  ioounsn  13608  lincmb01cmp  13626  iccf1o  13627  elfz1b  13727  ssfzoulel  13895  fzoopth  13897  modmuladd  14056  modaddmulmod  14081  ltexp2a  14309  leexp2  14314  ltexp2r  14316  exple1  14320  expnlbnd2  14378  mulsubdivbinom2  14406  fun2dmnop0  14649  ccatass  14734  swrdrn3  14802  ccatopth  14865  pfxccatin12lem2a  14876  repswpfx  14936  repswccat  14937  cshwidxmodr  14955  2cshw  14964  repsco  14991  s2f1o  15067  limsupgle  15644  limsupgre  15648  addcn2  15761  mulcn2  15763  binomrisefac  16208  dvdsval2  16425  dvdsadd2b  16476  dvdsmod  16499  oexpneg  16515  sadass  16641  gcdass  16720  rplpwr  16732  lcmass  16789  coprmdvds2  16829  rpmulgcd2  16831  rpdvds  16835  coprmprod  16836  cncongr2  16843  rpexp  16898  prmdiveq  16963  hashgcdlem  16965  odzdvds  16973  coprimeprodsq2  16987  pythagtriplem3  16996  pythagtriplem4  16997  pcdvdsb  17047  vdwnnlem1  17173  0ram  17198  ramz2  17202  ramub1lem1  17204  mremre  17774  mrieqv2d  17813  lubss  18687  lubun  18689  clatleglb  18692  clatglbss  18693  mrelatglb  18734  isnsgrp  18912  issubmnd  18953  gsumccat  19037  frmdss2  19059  submefmnd  19091  nmzsubg  19375  ghmnsgima  19454  gsmsymgreqlem1  19644  psgnunilem4  19711  odmodnn0  19754  odnncl  19759  odmod  19760  oddvds  19761  odeq  19764  odmulgid  19768  odmulgeq  19771  odbezout  19772  odf1o1  19786  odf1o2  19787  odngen  19791  gexdvdsi  19797  pgpfi1  19809  odcau  19818  subgslw  19830  fislw  19839  lsmless1x  19858  lsmless2x  19859  lsmsubm  19867  lsmmod  19889  lsmmod2  19890  efgsfo  19953  odadd1  20062  odadd2  20063  odadd  20064  lsmcomx  20070  prdscmnd  20075  gsumconst  20148  ablsimpgfindlem1  20323  csrgbinom  20458  ring1eq0  20529  mulgass2  20540  rngisom1  20696  rhmdvdsr  20758  cntzsubrng  20819  cntzsubr  20858  isdrng3lem2  21006  isabvd  21069  rmodislmod  21205  0lmhm  21315  lmhmvsca  21320  reslmhm2b  21329  pwssplit1  21334  pwssplit2  21335  pwssplit3  21336  lbspss  21357  lspsnat  21423  pidlnz  21528  lidldvgen  21658  xrsdsreclblem  21719  cssmre  21999  obs2ss  22035  uvcresum  22099  frlmsslsp  22102  frlmup4  22107  lindff1  22126  f1lindf  22128  lsslindf  22136  islindf4  22144  lindsenlbs  22157  issubassa  22175  evlsval2  22396  coe1subfv  22585  coe1sclmul  22601  coe1sclmul2  22603  mpomatmul  22761  mamutpos  22773  scmatscmide  22822  mavmulsolcl  22866  mulmarep1gsum2  22889  mdetdiaglem  22913  mdetdiag  22914  mdetunilem1  22927  mdetunilem3  22929  mdetunilem9  22935  maducoeval2  22955  madurid  22959  slesolinvbi  22999  cramerimplem1  23001  cramerlem1  23005  cramer  23009  cpmatel2  23031  m2cpm  23059  m2pmfzmap  23065  m2cpminvid2lem  23072  m2cpminvid2  23073  decpmatmul  23090  pmatcollpw1lem2  23093  pmatcollpw1  23094  pmatcollpw2lem  23095  pmatcollpwfi  23100  pm2mpcl  23115  mply1topmatcl  23123  mp2pm2mplem2  23125  mp2pm2mplem4  23127  mp2pm2mplem5  23128  mp2pm2mp  23129  pm2mpghmlem2  23130  pm2mpghmlem1  23131  chfacfisfcpmat  23173  topssnei  23442  cnconst2  23601  cnpresti  23606  cnprest2  23608  cnpdis  23611  cnt0  23664  cnt1  23668  cnhaus  23672  sscmp  23723  hauscmp  23725  cnconn  23740  unconn  23747  finlocfin  23839  comppfsc  23851  kgen2ss  23874  ptpjopn  23931  prdstopn  23947  ptrescn  23958  qtopss  24034  kqfvima  24049  fbssint  24157  fbasrn  24203  filuni  24204  fmss  24265  rnelfm  24272  fmufil  24278  fmco  24280  flimss2  24291  flimss1  24292  flimrest  24302  cnpflf2  24319  flfcnp  24323  supnfcls  24339  fclsss1  24341  fclsss2  24342  isfcf  24353  subgntr  24426  opnsubg  24427  cldsubg  24430  ghmcnp  24434  ustuqtop1  24560  bldisj  24717  blgt0  24718  bl2in  24719  blss2ps  24722  blss2  24723  blssps  24743  blss  24744  xmetresbl  24756  lpbl  24822  blcld  24824  stdbdmopn  24837  metcnp3  24859  metcnp  24860  metcnp2  24861  txmetcnp  24866  blval2  24881  nmoix  25048  nmoi2  25049  nmotri  25058  metdsge  25169  metdseq0  25174  iocopnst  25261  xrhmeo  25267  nmhmcn  25441  cphsqrtcl2  25507  cphsqrtcl3  25508  cssbn  25696  pjth  25760  ovoliunlem2  25824  volun  25866  mbfimaopn2  25978  iblconst  26138  limcvallem  26191  dvfval  26217  dvcnp2  26240  dvcn  26241  deg1mul3le  26435  deg1tmle  26436  dvdsq1p  26481  idomrootle  26491  ig1peu  26493  ig1pdvds  26498  ply1term  26522  coeid3  26559  dgrmulc  26590  dvply1  26605  aaliou2  26667  efcvx  26776  tanord  26866  eflogeq  26930  logdivlti  26948  logccv  26991  recxpcl  27003  cxplea  27024  cxpeq  27085  ang180  27142  isosctrlem2  27147  cxp2lim  27304  amgm  27318  muval1  27460  dvdssqf  27465  mumullem2  27507  mumul  27508  bcmono  27604  lgsneg  27648  lgsdilem  27651  lgsdirprm  27658  lgsdir  27659  lgsdi  27661  lgsne0  27662  nolesgn2o  28028  nogesgn1o  28030  nosep1o  28038  nosep2o  28039  nosepssdm  28043  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem4  28068  nosupbnd1lem5  28069  nosupbnd1lem6  28070  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem4  28083  noinfbnd1lem6  28085  noinfbnd2  28088  noetasuplem3  28092  noetainflem3  28096  leslss  28295  cofslts  28304  coinitslts  28305  cofcutrtime  28313  addsass  28391  addsdi  28541  mulsass  28552  ltmuls2  28557  divmulsw  28579  bdayfinbndlem1  28853  z12bdaylem  28870  brbtwn2  29483  colinearalglem1  29484  colinearalg  29488  axcgrtr  29493  axsegconlem8  29502  axsegconlem9  29503  axsegconlem10  29504  axcontlem2  29543  axcontlem10  29551  elntg2  29563  ewlkle  30186  crctcshwlkn0lem5  30403  wwlknp  30432  wwlksnext  30482  wwlksnextproplem1  30498  wspthsnwspthsnon  30505  clwlkclwwlklem3  30592  erclwwlksym  30612  erclwwlknsym  30661  upgriseupth  30808  eucrct2eupth  30846  3cyclfrgrrn  30887  numclwwlk2lem1lem  30943  numclwwlk1lem2foa  30955  frgrregord13  30997  nvmul0or  31252  ipval2lem2  31306  lnoadd  31360  lnosub  31361  lnomul  31362  shless  31961  shlej1  31962  kbmul  32557  homco2  32579  kbass2  32719  eliccelico  33369  elicoelioo  33370  iocinioc2  33371  iocinif  33373  difioo  33374  nexple  33424  swrdrn2  33517  xrge0adddir  33579  xrge0npcan  33581  isarchi2  33746  archiabl  33759  lindssn  33933  ssmxidl  33999  pstmfval  34528  fmcncfil  34563  zrhnm  34599  qqhnm  34622  volfiniune  34863  dya2iocnrect  34913  probinc  35053  cndprob01  35067  signswmnd  35186  bnj517  35515  cvmsss2  36039  cvmlift2lem10  36077  br6  36522  funsseq  36533  cgrtriv  36767  5segofs  36771  btwnouttr2  36787  btwnxfr  36821  lineext  36841  btwnconn1lem13  36864  brsegle2  36874  nmulss1  36963  ltnmul  36965  nmulle  36966  ltnadd  36967  naddle  36968  nadddi  36973  nn0prpwlem  37110  weiunpo  37253  weiunso  37254  weiunfr  37255  weiunse  37256  axtcond  37266  blbnd  38722  ismtyima  38738  rrndstprj2  38766  ghomdiv  38827  grpokerinj  38828  lsatfixedN  40067  lssat  40074  lshpkrlem4  40171  cvrcon3b  40335  atlen0  40368  atcvreq0  40372  atnle  40375  atlatmstc  40377  atlatle  40378  cvlcvr1  40397  hlsupr2  40445  hlrelat2  40461  cvrexchlem  40477  lnnat  40485  atcvrj2b  40490  3dimlem3  40519  3dim1  40525  1cvrjat  40533  llni  40566  llni2  40570  llnexatN  40579  2llnmat  40582  lplni  40590  2atnelpln  40602  llncvrlpln2  40615  2llnmj  40618  lplnexatN  40621  lplnexllnN  40622  2llnm3N  40627  lvoli  40633  lvoli3  40635  lvolnle3at  40640  islvol2aN  40650  4atlem4a  40657  4atlem4b  40658  4atlem11  40667  lplncvrlvol2  40673  2lplnmj  40680  islinei  40798  linepmap  40833  lnjatN  40838  lncvrat  40840  lncmp  40841  elpaddn0  40858  elpaddatriN  40861  elpaddat  40862  paddcom  40871  paddss2  40876  paddss12  40877  paddasslem4  40881  paddasslem9  40886  paddasslem10  40887  pmodl42N  40909  pmapjoin  40910  llnmod1i2  40918  polcon2bN  40978  pclfinclN  41008  poml4N  41011  poml6N  41013  osumcllem1N  41014  osumcllem2N  41015  osumcllem11N  41024  osumclN  41025  pmapojoinN  41026  pexmidlem2N  41029  pexmidlem3N  41030  pexmidlem4N  41031  pexmidlem6N  41033  pexmidlem7N  41034  pl42lem2N  41038  pl42lem3N  41039  pl42lem4N  41040  pl42N  41041  lhprelat3N  41098  4atex  41134  lauteq  41153  lautco  41155  ltrncoidN  41186  ltrneq2  41206  ltrnideq  41233  trlnle  41244  trlval3  41245  cdlemc  41255  cdlemd9  41264  cdlemd  41265  cdleme21j  41394  cdleme21  41395  cdleme29ex  41432  cdlemefr27cl  41461  cdlemefs27cl  41471  cdleme32d  41502  cdleme32f  41504  cdleme35h2  41515  cdleme40m  41525  cdleme17d3  41554  cdleme48fvg  41558  cdlemeg46fvcl  41564  cdlemeg46fgN  41592  cdleme48fgv  41596  cdleme50trn3  41611  cdlemb3  41664  cdlemg8  41689  cdlemg11a  41695  cdlemg15a  41713  cdlemg15  41714  cdlemg16  41715  cdlemg16z  41717  cdlemg17dN  41721  cdlemg24  41746  cdlemg37  41747  cdlemg29  41763  cdlemg33b  41765  cdlemg38  41773  cdlemg40  41775  trlco  41785  cdlemg44b  41790  ltrncom  41796  trljco  41798  tendococl  41830  tendoplcl  41839  tendoplcom  41840  cdlemj2  41880  tendoid0  41883  tendo1ne0  41886  cdlemk25-3  41962  cdlemk36  41971  cdlemkid4  41992  cdlemk19x  42001  cdlemk53  42015  cdlemk56  42029  cdleml5N  42038  tendospcanN  42081  cdlemm10N  42176  dihord6apre  42314  dihord  42322  dihmeetlem1N  42348  dihglblem2N  42352  dihmeetlem2N  42357  dihmeetbN  42361  dihmeetlem5  42366  dihmeetlem6  42367  dihmeetlem7N  42368  dihmeetlem10N  42374  dihmeetlem12N  42376  dihmeetlem16N  42380  dihmeetlem17N  42381  dihmeetlem18N  42382  dihmeetALTN  42385  dihlspsnssN  42390  dvh3dim2  42506  dvh3dim3N  42507  lcfrlem16  42616  mapdrvallem2  42703  mapdh8ad  42837  hgmapvvlem3  42983  sticksstones1  43197  sticksstones2  43198  aks6d1c6isolem1  43225  resubcan2  43440  diophrw  43770  eldioph2lem1  43771  diophrex  43786  rencldnfi  43828  pellexlem2  43837  pellqrexplicit  43884  infmrgelbi  43885  pellfundglb  43892  pellfund14gap  43894  rmxycomplete  43924  congadd  43973  acongeq  43990  jm2.19  44000  jm2.23  44003  jm2.20nn  44004  jm2.27  44015  jm3.1  44027  lnmepi  44087  lmhmlnmsplit  44089  hbtlem2  44126  dgraa0p  44151  proot1hash  44197  iocunico  44213  iocinico  44214  oasubex  44288  cantnf2  44327  onmcl  44333  omcl2  44335  nadd2rabex  44388  nadd1rabtr  44390  nadd1rabex  44392  fzunt  44456  relexpxpmin  44717  ntrclsk3  45070  grur1cld  45230  ismnu  45245  grumnudlem  45269  ismnushort  45285  rfcnnnub  46053  uzwo4  46070  wessf1ornlem  46200  supxrge  46350  infleinflem2  46382  iccintsng  46535  climsuse  46620  lptre2pt  46650  limcleqr  46654  0ellimcdiv  46659  fnlimfvre  46684  dvnprodlem1  46956  volioc  46982  stoweidlem17  47027  stoweidlem19  47029  stoweidlem20  47030  stoweidlem22  47032  stoweidlem28  47038  stoweidlem34  47044  stoweidlem44  47054  stoweidlem60  47070  wallispilem3  47077  fourierdlem42  47159  fourierdlem48  47164  fourierdlem51  47167  fourierdlem54  47170  fourierdlem74  47190  fourierdlem77  47193  fourierdlem87  47203  fourierdlem97  47213  ioorrnopnlem  47314  ovnsubaddlem2  47581  smfinflem  47827  fsupdm  47852  finfdm  47856  eluzge0nn0  48382  fzopredsuc  48394  imasetpreimafvbijlemfv  48484  lighneallem4  48695  oexpnegALTV  48775  oexpnegnz  48776  tgblthelfgott  48913  clnbgrgrim  49032  isubgr3stgrlem3  49066  rmsupp0  49480  rmsuppss  49482  lincresunit3lem3  49586  lincresunit3lem2  49592  lindssnlvec  49598  fdivmptf  49653  refdivmptf  49654  elbigolo1  49669  rrx2linest  49854  itsclc0lem1  49868  itsclc0lem2  49869  itsclc0yqsollem1  49874  itsclc0b  49884  setc1onsubc  50710