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  3596  2nreu  4405  f1prex  7288  weniso  7360  ofmpteq  7704  tfisi  7858  mposn  8103  fprlem1  8302  smogt  8359  smocdmdom  8360  omeulem1  8572  nnmord  8623  nnmword  8624  naddasslem1  8686  naddasslem2  8687  difsnen  9060  enfixsn  9087  mapunen  9147  ac6sfi  9257  ordiso2  9490  wemaplem2  9522  wemapso2lem  9527  en2eqpr  10013  acndom  10057  infmap2  10222  cflim2  10268  cfsmolem  10275  coftr  10278  fin23lem26  10330  isf32lem9  10366  fin1a2lem9  10413  fin1a2lem10  10414  gchdomtri  10641  canth4  10659  gchpwdom  10682  gruima  10814  grudomon  10829  prn0  11001  distrlem4pr  11038  prlem934  11045  addcan  11421  addcan2  11422  divmulass  11922  divmulasscom  11923  ltmul1a  12091  supmul1  12211  uzsupss  12992  xaddass  13303  xleadd1a  13307  xlesubadd  13317  xmulass  13341  xlemul2a  13343  xadddilem  13348  xadddi  13349  ixxdisj  13415  ixxun  13416  ixxlb  13422  icoshftf1o  13529  icodisj  13531  ioounsn  13532  lincmb01cmp  13550  iccf1o  13551  elfz1b  13650  ssfzoulel  13818  fzoopth  13820  modmuladd  13979  modaddmulmod  14004  ltexp2a  14232  leexp2  14237  ltexp2r  14239  exple1  14243  expnlbnd2  14300  mulsubdivbinom2  14328  fun2dmnop0  14571  ccatass  14656  swrdrn3  14724  ccatopth  14787  pfxccatin12lem2a  14798  repswpfx  14858  repswccat  14859  cshwidxmodr  14877  2cshw  14886  repsco  14913  s2f1o  14989  limsupgle  15566  limsupgre  15570  addcn2  15683  mulcn2  15685  binomrisefac  16132  dvdsval2  16349  dvdsadd2b  16400  dvdsmod  16423  oexpneg  16439  sadass  16565  gcdass  16641  rplpwr  16652  lcmass  16708  coprmdvds2  16748  rpmulgcd2  16750  rpdvds  16754  coprmprod  16755  cncongr2  16762  rpexp  16817  prmdiveq  16881  hashgcdlem  16883  odzdvds  16891  coprimeprodsq2  16905  pythagtriplem3  16914  pythagtriplem4  16915  pcdvdsb  16965  vdwnnlem1  17091  0ram  17116  ramz2  17120  ramub1lem1  17122  mremre  17692  mrieqv2d  17731  lubss  18605  lubun  18607  clatleglb  18610  clatglbss  18611  mrelatglb  18652  isnsgrp  18829  issubmnd  18870  gsumccat  18954  frmdss2  18976  submefmnd  19008  nmzsubg  19292  ghmnsgima  19371  gsmsymgreqlem1  19561  psgnunilem4  19628  odmodnn0  19671  odnncl  19676  odmod  19677  oddvds  19678  odeq  19681  odmulgid  19685  odmulgeq  19688  odbezout  19689  odf1o1  19703  odf1o2  19704  odngen  19708  gexdvdsi  19714  pgpfi1  19726  odcau  19735  subgslw  19747  fislw  19756  lsmless1x  19775  lsmless2x  19776  lsmsubm  19784  lsmmod  19806  lsmmod2  19807  efgsfo  19870  odadd1  19979  odadd2  19980  odadd  19981  lsmcomx  19987  prdscmnd  19992  gsumconst  20065  ablsimpgfindlem1  20240  csrgbinom  20375  ring1eq0  20444  mulgass2  20455  rngisom1  20611  rhmdvdsr  20672  cntzsubrng  20733  cntzsubr  20772  isdrng3lem2  20919  isabvd  20982  rmodislmod  21118  0lmhm  21228  lmhmvsca  21233  reslmhm2b  21242  pwssplit1  21247  pwssplit2  21248  pwssplit3  21249  lbspss  21270  lspsnat  21336  pidlnz  21441  lidldvgen  21569  xrsdsreclblem  21630  cssmre  21910  obs2ss  21946  uvcresum  22010  frlmsslsp  22013  frlmup4  22018  lindff1  22037  f1lindf  22039  lsslindf  22047  islindf4  22055  lindsenlbs  22068  issubassa  22086  evlsval2  22307  coe1subfv  22496  coe1sclmul  22512  coe1sclmul2  22514  mpomatmul  22672  mamutpos  22684  scmatscmide  22733  mavmulsolcl  22777  mulmarep1gsum2  22800  mdetdiaglem  22824  mdetdiag  22825  mdetunilem1  22838  mdetunilem3  22840  mdetunilem9  22846  maducoeval2  22866  madurid  22870  slesolinvbi  22910  cramerimplem1  22912  cramerlem1  22916  cramer  22920  cpmatel2  22942  m2cpm  22970  m2pmfzmap  22976  m2cpminvid2lem  22983  m2cpminvid2  22984  decpmatmul  23001  pmatcollpw1lem2  23004  pmatcollpw1  23005  pmatcollpw2lem  23006  pmatcollpwfi  23011  pm2mpcl  23026  mply1topmatcl  23034  mp2pm2mplem2  23036  mp2pm2mplem4  23038  mp2pm2mplem5  23039  mp2pm2mp  23040  pm2mpghmlem2  23041  pm2mpghmlem1  23042  chfacfisfcpmat  23084  topssnei  23353  cnconst2  23512  cnpresti  23517  cnprest2  23519  cnpdis  23522  cnt0  23575  cnt1  23579  cnhaus  23583  sscmp  23634  hauscmp  23636  cnconn  23651  unconn  23658  finlocfin  23750  comppfsc  23762  kgen2ss  23785  ptpjopn  23842  prdstopn  23858  ptrescn  23869  qtopss  23945  kqfvima  23960  fbssint  24068  fbasrn  24114  filuni  24115  fmss  24176  rnelfm  24183  fmufil  24189  fmco  24191  flimss2  24202  flimss1  24203  flimrest  24213  cnpflf2  24230  flfcnp  24234  supnfcls  24250  fclsss1  24252  fclsss2  24253  isfcf  24264  subgntr  24337  opnsubg  24338  cldsubg  24341  ghmcnp  24345  ustuqtop1  24471  bldisj  24628  blgt0  24629  bl2in  24630  blss2ps  24633  blss2  24634  blssps  24654  blss  24655  xmetresbl  24667  lpbl  24733  blcld  24735  stdbdmopn  24748  metcnp3  24770  metcnp  24771  metcnp2  24772  txmetcnp  24777  blval2  24792  nmoix  24959  nmoi2  24960  nmotri  24969  metdsge  25080  metdseq0  25085  iocopnst  25172  xrhmeo  25178  nmhmcn  25352  cphsqrtcl2  25418  cphsqrtcl3  25419  cssbn  25607  pjth  25671  ovoliunlem2  25735  volun  25777  mbfimaopn2  25889  iblconst  26050  limcvallem  26103  dvfval  26129  dvcnp2  26152  dvcn  26153  deg1mul3le  26347  deg1tmle  26348  dvdsq1p  26393  idomrootle  26403  ig1peu  26405  ig1pdvds  26410  ply1term  26434  coeid3  26470  dgrmulc  26501  dvply1  26518  aaliou2  26576  efcvx  26685  tanord  26776  eflogeq  26840  logdivlti  26858  logccv  26901  recxpcl  26913  cxplea  26934  cxpeq  26995  ang180  27052  isosctrlem2  27057  cxp2lim  27214  amgm  27228  muval1  27370  dvdssqf  27375  mumullem2  27417  mumul  27418  bcmono  27514  lgsneg  27558  lgsdilem  27561  lgsdirprm  27568  lgsdir  27569  lgsdi  27571  lgsne0  27572  nolesgn2o  27908  nogesgn1o  27910  nosep1o  27918  nosep2o  27919  nosepssdm  27923  nosupres  27944  nosupbnd1lem1  27945  nosupbnd1lem4  27948  nosupbnd1lem5  27949  nosupbnd1lem6  27950  noinfres  27959  noinfbnd1lem1  27960  noinfbnd1lem4  27963  noinfbnd1lem6  27965  noinfbnd2  27968  noetasuplem3  27972  noetainflem3  27976  leslss  28175  cofslts  28184  coinitslts  28185  cofcutrtime  28193  addsass  28271  addsdi  28421  mulsass  28432  ltmuls2  28437  divmulsw  28459  bdayfinbndlem1  28733  z12bdaylem  28750  brbtwn2  29363  colinearalglem1  29364  colinearalg  29368  axcgrtr  29373  axsegconlem8  29382  axsegconlem9  29383  axsegconlem10  29384  axcontlem2  29423  axcontlem10  29431  elntg2  29443  ewlkle  30066  crctcshwlkn0lem5  30283  wwlknp  30312  wwlksnext  30362  wwlksnextproplem1  30378  wspthsnwspthsnon  30385  clwlkclwwlklem3  30472  erclwwlksym  30492  erclwwlknsym  30541  upgriseupth  30688  eucrct2eupth  30726  3cyclfrgrrn  30767  numclwwlk2lem1lem  30823  numclwwlk1lem2foa  30835  frgrregord13  30877  nvmul0or  31132  ipval2lem2  31186  lnoadd  31240  lnosub  31241  lnomul  31242  shless  31841  shlej1  31842  kbmul  32437  homco2  32459  kbass2  32599  eliccelico  33250  elicoelioo  33251  iocinioc2  33252  iocinif  33254  difioo  33255  nexple  33305  swrdrn2  33398  xrge0adddir  33460  xrge0npcan  33462  isarchi2  33627  archiabl  33640  lindssn  33813  ssmxidl  33879  pstmfval  34408  fmcncfil  34443  zrhnm  34479  qqhnm  34502  volfiniune  34743  dya2iocnrect  34794  probinc  34934  cndprob01  34948  signswmnd  35067  bnj517  35396  cvmsss2  35855  cvmlift2lem10  35893  br6  36338  funsseq  36349  cgrtriv  36584  5segofs  36588  btwnouttr2  36604  btwnxfr  36638  lineext  36658  btwnconn1lem13  36681  brsegle2  36691  nmulss1  36796  ltnmul  36798  nmulle  36799  ltnadd  36800  naddle  36801  nadddi  36806  nn0prpwlem  36943  weiunpo  37086  weiunso  37087  weiunfr  37088  weiunse  37089  axtcond  37099  blbnd  38539  ismtyima  38555  rrndstprj2  38583  ghomdiv  38644  grpokerinj  38645  lsatfixedN  39884  lssat  39891  lshpkrlem4  39988  cvrcon3b  40152  atlen0  40185  atcvreq0  40189  atnle  40192  atlatmstc  40194  atlatle  40195  cvlcvr1  40214  hlsupr2  40262  hlrelat2  40278  cvrexchlem  40294  lnnat  40302  atcvrj2b  40307  3dimlem3  40336  3dim1  40342  1cvrjat  40350  llni  40383  llni2  40387  llnexatN  40396  2llnmat  40399  lplni  40407  2atnelpln  40419  llncvrlpln2  40432  2llnmj  40435  lplnexatN  40438  lplnexllnN  40439  2llnm3N  40444  lvoli  40450  lvoli3  40452  lvolnle3at  40457  islvol2aN  40467  4atlem4a  40474  4atlem4b  40475  4atlem11  40484  lplncvrlvol2  40490  2lplnmj  40497  islinei  40615  linepmap  40650  lnjatN  40655  lncvrat  40657  lncmp  40658  elpaddn0  40675  elpaddatriN  40678  elpaddat  40679  paddcom  40688  paddss2  40693  paddss12  40694  paddasslem4  40698  paddasslem9  40703  paddasslem10  40704  pmodl42N  40726  pmapjoin  40727  llnmod1i2  40735  polcon2bN  40795  pclfinclN  40825  poml4N  40828  poml6N  40830  osumcllem1N  40831  osumcllem2N  40832  osumcllem11N  40841  osumclN  40842  pmapojoinN  40843  pexmidlem2N  40846  pexmidlem3N  40847  pexmidlem4N  40848  pexmidlem6N  40850  pexmidlem7N  40851  pl42lem2N  40855  pl42lem3N  40856  pl42lem4N  40857  pl42N  40858  lhprelat3N  40915  4atex  40951  lauteq  40970  lautco  40972  ltrncoidN  41003  ltrneq2  41023  ltrnideq  41050  trlnle  41061  trlval3  41062  cdlemc  41072  cdlemd9  41081  cdlemd  41082  cdleme21j  41211  cdleme21  41212  cdleme29ex  41249  cdlemefr27cl  41278  cdlemefs27cl  41288  cdleme32d  41319  cdleme32f  41321  cdleme35h2  41332  cdleme40m  41342  cdleme17d3  41371  cdleme48fvg  41375  cdlemeg46fvcl  41381  cdlemeg46fgN  41409  cdleme48fgv  41413  cdleme50trn3  41428  cdlemb3  41481  cdlemg8  41506  cdlemg11a  41512  cdlemg15a  41530  cdlemg15  41531  cdlemg16  41532  cdlemg16z  41534  cdlemg17dN  41538  cdlemg24  41563  cdlemg37  41564  cdlemg29  41580  cdlemg33b  41582  cdlemg38  41590  cdlemg40  41592  trlco  41602  cdlemg44b  41607  ltrncom  41613  trljco  41615  tendococl  41647  tendoplcl  41656  tendoplcom  41657  cdlemj2  41697  tendoid0  41700  tendo1ne0  41703  cdlemk25-3  41779  cdlemk36  41788  cdlemkid4  41809  cdlemk19x  41818  cdlemk53  41832  cdlemk56  41846  cdleml5N  41855  tendospcanN  41898  cdlemm10N  41993  dihord6apre  42131  dihord  42139  dihmeetlem1N  42165  dihglblem2N  42169  dihmeetlem2N  42174  dihmeetbN  42178  dihmeetlem5  42183  dihmeetlem6  42184  dihmeetlem7N  42185  dihmeetlem10N  42191  dihmeetlem12N  42193  dihmeetlem16N  42197  dihmeetlem17N  42198  dihmeetlem18N  42199  dihmeetALTN  42202  dihlspsnssN  42207  dvh3dim2  42323  dvh3dim3N  42324  lcfrlem16  42433  mapdrvallem2  42520  mapdh8ad  42654  hgmapvvlem3  42800  sticksstones1  43014  sticksstones2  43015  aks6d1c6isolem1  43042  resubcan2  43265  diophrw  43606  eldioph2lem1  43607  diophrex  43622  rencldnfi  43664  pellexlem2  43673  pellqrexplicit  43720  infmrgelbi  43721  pellfundglb  43728  pellfund14gap  43730  rmxycomplete  43760  congadd  43809  acongeq  43826  jm2.19  43836  jm2.23  43839  jm2.20nn  43840  jm2.27  43851  jm3.1  43863  lnmepi  43928  lmhmlnmsplit  43930  hbtlem2  43967  dgraa0p  43992  proot1hash  44038  iocunico  44054  iocinico  44055  oasubex  44129  cantnf2  44168  onmcl  44174  omcl2  44176  nadd2rabex  44229  nadd1rabtr  44231  nadd1rabex  44233  fzunt  44297  relexpxpmin  44559  ntrclsk3  44912  grur1cld  45072  ismnu  45087  grumnudlem  45111  ismnushort  45127  rfcnnnub  45872  uzwo4  45889  wessf1ornlem  46019  supxrge  46170  infleinflem2  46202  iccintsng  46355  climsuse  46440  lptre2pt  46470  limcleqr  46474  0ellimcdiv  46479  fnlimfvre  46504  dvnprodlem1  46776  volioc  46802  stoweidlem17  46847  stoweidlem19  46849  stoweidlem20  46850  stoweidlem22  46852  stoweidlem28  46858  stoweidlem34  46864  stoweidlem44  46874  stoweidlem60  46890  wallispilem3  46897  fourierdlem42  46979  fourierdlem48  46984  fourierdlem51  46987  fourierdlem54  46990  fourierdlem74  47010  fourierdlem77  47013  fourierdlem87  47023  fourierdlem97  47033  ioorrnopnlem  47134  ovnsubaddlem2  47401  smfinflem  47647  fsupdm  47672  finfdm  47676  eluzge0nn0  48202  fzopredsuc  48214  imasetpreimafvbijlemfv  48304  lighneallem4  48515  oexpnegALTV  48595  oexpnegnz  48596  tgblthelfgott  48733  clnbgrgrim  48852  isubgr3stgrlem3  48886  rmsupp0  49300  rmsuppss  49302  lincresunit3lem3  49406  lincresunit3lem2  49412  lindssnlvec  49418  fdivmptf  49473  refdivmptf  49474  elbigolo1  49489  rrx2linest  49674  itsclc0lem1  49688  itsclc0lem2  49689  itsclc0yqsollem1  49694  itsclc0b  49704  setc1onsubc  50530