Theorem simpl2 1189

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  simpl12  1246  simpl22  1249  simpl32  1252  simp1l2  1264  simp2l2  1270  simp3l2  1276  3anandirs  1468  rspc3ev  3623  2nreu  4443  f1prex  7293  weniso  7361  ofmpteq  7707  tfisi  7864  mposn  8108  fprlem1  8306  smogt  8388  smocdmdom  8389  omeulem1  8603  nnmord  8653  nnmword  8654  naddasslem1  8715  naddasslem2  8716  difsnen  9078  enfixsn  9106  mapunen  9171  ac6sfi  9312  ordiso2  9540  wemaplem2  9572  wemapso2lem  9577  en2eqpr  10032  acndom  10076  infmap2  10243  cflim2  10288  cfsmolem  10295  coftr  10298  fin23lem26  10350  isf32lem9  10386  fin1a2lem9  10433  fin1a2lem10  10434  gchdomtri  10654  canth4  10672  gchpwdom  10695  gruima  10827  grudomon  10842  prn0  11014  distrlem4pr  11051  prlem934  11058  addcan  11430  addcan2  11431  divmulass  11928  divmulasscom  11929  ltmul1a  12096  supmul1  12216  uzsupss  12957  xaddass  13263  xleadd1a  13267  xlesubadd  13277  xmulass  13301  xlemul2a  13303  xadddilem  13308  xadddi  13309  ixxdisj  13374  ixxun  13375  ixxlb  13381  icoshftf1o  13486  icodisj  13488  ioounsn  13489  lincmb01cmp  13507  iccf1o  13508  elfz1b  13605  ssfzoulel  13761  fzoopth  13763  modmuladd  13914  modaddmulmod  13939  ltexp2a  14166  leexp2  14171  ltexp2r  14173  exple1  14176  expnlbnd2  14232  mulsubdivbinom2  14257  fun2dmnop0  14491  ccatass  14574  ccatopth  14702  pfxccatin12lem2a  14713  repswpfx  14771  repswccat  14772  cshwidxmodr  14790  2cshw  14799  repsco  14827  s2f1o  14903  limsupgle  15457  limsupgre  15461  addcn2  15574  mulcn2  15576  binomrisefac  16022  dvdsval2  16237  dvdsadd2b  16286  dvdsmod  16309  oexpneg  16325  sadass  16449  gcdass  16526  rplpwr  16536  lcmass  16588  coprmdvds2  16628  rpmulgcd2  16630  rpdvds  16634  coprmprod  16635  cncongr2  16642  rpexp  16697  prmdiveq  16758  hashgcdlem  16760  odzdvds  16767  coprimeprodsq2  16781  pythagtriplem3  16790  pythagtriplem4  16791  pcdvdsb  16841  vdwnnlem1  16967  0ram  16992  ramz2  16996  ramub1lem1  16998  mremre  17587  mrieqv2d  17622  lubss  18508  lubun  18510  clatleglb  18513  clatglbss  18514  mrelatglb  18555  isnsgrp  18686  issubmnd  18724  gsumccat  18801  frmdss2  18823  submefmnd  18855  nmzsubg  19128  ghmnsgima  19203  gsmsymgreqlem1  19397  psgnunilem4  19464  odmodnn0  19507  odnncl  19512  odmod  19513  oddvds  19514  odeq  19517  odmulgid  19521  odmulgeq  19524  odbezout  19525  odf1o1  19539  odf1o2  19540  odngen  19544  gexdvdsi  19550  pgpfi1  19562  odcau  19571  subgslw  19583  fislw  19592  lsmless1x  19611  lsmless2x  19612  lsmsubm  19620  lsmmod  19642  lsmmod2  19643  efgsfo  19706  odadd1  19815  odadd2  19816  odadd  19817  lsmcomx  19823  prdscmnd  19828  gsumconst  19901  ablsimpgfindlem1  20076  srg1zr  20167  csrgbinom  20184  ring1eq0  20246  mulgass2  20257  rngisom1  20417  rhmdvdsr  20459  cntzsubrng  20516  cntzsubr  20557  isabvd  20712  rmodislmod  20825  rmodislmodOLD  20826  0lmhm  20937  lmhmvsca  20942  reslmhm2b  20951  pwssplit1  20956  pwssplit2  20957  pwssplit3  20958  lbspss  20979  lspsnat  21045  lidldvgen  21241  xrsdsreclblem  21362  cssmre  21642  obs2ss  21680  uvcresum  21744  frlmsslsp  21747  frlmup4  21752  lindff1  21771  f1lindf  21773  lsslindf  21781  islindf4  21789  issubassa  21817  evlsval2  22055  coe1subfv  22210  coe1sclmul  22226  coe1sclmul2  22228  mpomatmul  22392  mamutpos  22404  scmatscmide  22453  mavmulsolcl  22497  mulmarep1gsum2  22520  mdetdiaglem  22544  mdetdiag  22545  mdetunilem1  22558  mdetunilem3  22560  mdetunilem9  22566  maducoeval2  22586  madurid  22590  slesolinvbi  22627  cramerimplem1  22629  cramerlem1  22633  cramer  22637  cpmatel2  22659  m2cpm  22687  m2pmfzmap  22693  m2cpminvid2lem  22700  m2cpminvid2  22701  decpmatmul  22718  pmatcollpw1lem2  22721  pmatcollpw1  22722  pmatcollpw2lem  22723  pmatcollpwfi  22728  pm2mpcl  22743  mply1topmatcl  22751  mp2pm2mplem2  22753  mp2pm2mplem4  22755  mp2pm2mplem5  22756  mp2pm2mp  22757  pm2mpghmlem2  22758  pm2mpghmlem1  22759  chfacfisfcpmat  22801  topssnei  23072  cnconst2  23231  cnpresti  23236  cnprest2  23238  cnpdis  23241  cnt0  23294  cnt1  23298  cnhaus  23302  sscmp  23353  hauscmp  23355  cnconn  23370  unconn  23377  finlocfin  23468  comppfsc  23480  kgen2ss  23503  ptpjopn  23560  prdstopn  23576  ptrescn  23587  qtopss  23663  kqfvima  23678  fbssint  23786  fbasrn  23832  filuni  23833  fmss  23894  rnelfm  23901  fmufil  23907  fmco  23909  flimss2  23920  flimss1  23921  flimrest  23931  cnpflf2  23948  flfcnp  23952  supnfcls  23968  fclsss1  23970  fclsss2  23971  isfcf  23982  subgntr  24055  opnsubg  24056  cldsubg  24059  ghmcnp  24063  ustuqtop1  24190  bldisj  24348  blgt0  24349  bl2in  24350  blss2ps  24353  blss2  24354  blssps  24374  blss  24375  xmetresbl  24387  lpbl  24456  blcld  24458  stdbdmopn  24471  metcnp3  24493  metcnp  24494  metcnp2  24495  txmetcnp  24500  blval2  24515  nmoix  24690  nmoi2  24691  nmotri  24700  metdsge  24809  metdseq0  24814  iocopnst  24908  xrhmeo  24915  nmhmcn  25091  cphsqrtcl2  25158  cphsqrtcl3  25159  cssbn  25347  pjth  25411  ovoliunlem2  25476  volun  25518  mbfimaopn2  25630  iblconst  25791  limcvallem  25844  dvfval  25870  dvcnp2  25893  dvcnp2OLD  25894  dvcn  25895  deg1mul3le  26097  deg1tmle  26098  dvdsq1p  26142  idomrootle  26152  ig1peu  26154  ig1pdvds  26159  ply1term  26183  coeid3  26219  dgrmulc  26251  dvply1  26263  aaliou2  26320  efcvx  26431  tanord  26517  eflogeq  26581  logdivlti  26599  logccv  26642  recxpcl  26654  cxplea  26675  cxpeq  26737  ang180  26791  isosctrlem2  26796  cxp2lim  26954  amgm  26968  muval1  27110  dvdssqf  27115  mumullem2  27157  mumul  27158  bcmono  27255  lgsneg  27299  lgsdilem  27302  lgsdirprm  27309  lgsdir  27310  lgsdi  27312  lgsne0  27313  nolesgn2o  27650  nogesgn1o  27652  nosep1o  27660  nosep2o  27661  nosepssdm  27665  nosupres  27686  nosupbnd1lem1  27687  nosupbnd1lem4  27690  nosupbnd1lem5  27691  nosupbnd1lem6  27692  noinfres  27701  noinfbnd1lem1  27702  noinfbnd1lem4  27705  noinfbnd1lem6  27707  noinfbnd2  27710  noetasuplem3  27714  noetainflem3  27718  slelss  27880  cofsslt  27884  coinitsslt  27885  cofcutrtime  27893  addsass  27968  addsdi  28105  mulsass  28116  sltmul2  28121  divsmulw  28142  brbtwn2  28788  colinearalglem1  28789  colinearalg  28793  axcgrtr  28798  axsegconlem8  28807  axsegconlem9  28808  axsegconlem10  28809  axcontlem2  28848  axcontlem10  28856  elntg2  28868  ewlkle  29491  crctcshwlkn0lem5  29697  wwlknp  29726  wwlksnext  29776  wwlksnextproplem1  29792  wspthsnwspthsnon  29799  clwlkclwwlklem3  29883  erclwwlksym  29903  erclwwlknsym  29952  upgriseupth  30089  eucrct2eupth  30127  3cyclfrgrrn  30168  numclwwlk2lem1lem  30224  numclwwlk1lem2foa  30236  frgrregord13  30278  nvmul0or  30532  ipval2lem2  30586  lnoadd  30640  lnosub  30641  lnomul  30642  shless  31241  shlej1  31242  kbmul  31837  homco2  31859  kbass2  31999  eliccelico  32627  elicoelioo  32628  iocinioc2  32629  iocinif  32631  difioo  32632  swrdrn2  32764  swrdrn3  32765  xrge0adddir  32837  xrge0npcan  32839  isarchi2  32985  archiabl  32998  pidlnz  33188  lindssn  33190  ssmxidl  33286  pstmfval  33628  fmcncfil  33663  zrhnm  33701  qqhnm  33722  nexple  33759  volfiniune  33980  dya2iocnrect  34032  probinc  34172  cndprob01  34186  signswmnd  34320  bnj517  34647  cvmsss2  35015  cvmlift2lem10  35053  br6  35482  funsseq  35494  cgrtriv  35729  5segofs  35733  btwnouttr2  35749  btwnxfr  35783  lineext  35803  btwnconn1lem13  35826  brsegle2  35836  nn0prpwlem  35937  lindsenlbs  37219  blbnd  37391  ismtyima  37407  rrndstprj2  37435  ghomdiv  37496  grpokerinj  37497  lsatfixedN  38611  lssat  38618  lshpkrlem4  38715  cvrcon3b  38879  atlen0  38912  atcvreq0  38916  atnle  38919  atlatmstc  38921  atlatle  38922  cvlcvr1  38941  hlsupr2  38990  hlrelat2  39006  cvrexchlem  39022  lnnat  39030  atcvrj2b  39035  3dimlem3  39064  3dim1  39070  1cvrjat  39078  llni  39111  llni2  39115  llnexatN  39124  2llnmat  39127  lplni  39135  2atnelpln  39147  llncvrlpln2  39160  2llnmj  39163  lplnexatN  39166  lplnexllnN  39167  2llnm3N  39172  lvoli  39178  lvoli3  39180  lvolnle3at  39185  islvol2aN  39195  4atlem4a  39202  4atlem4b  39203  4atlem11  39212  lplncvrlvol2  39218  2lplnmj  39225  islinei  39343  linepmap  39378  lnjatN  39383  lncvrat  39385  lncmp  39386  elpaddn0  39403  elpaddatriN  39406  elpaddat  39407  paddcom  39416  paddss2  39421  paddss12  39422  paddasslem4  39426  paddasslem9  39431  paddasslem10  39432  pmodl42N  39454  pmapjoin  39455  llnmod1i2  39463  polcon2bN  39523  pclfinclN  39553  poml4N  39556  poml6N  39558  osumcllem1N  39559  osumcllem2N  39560  osumcllem11N  39569  osumclN  39570  pmapojoinN  39571  pexmidlem2N  39574  pexmidlem3N  39575  pexmidlem4N  39576  pexmidlem6N  39578  pexmidlem7N  39579  pl42lem2N  39583  pl42lem3N  39584  pl42lem4N  39585  pl42N  39586  lhprelat3N  39643  4atex  39679  lauteq  39698  lautco  39700  ltrncoidN  39731  ltrneq2  39751  ltrnideq  39778  trlnle  39789  trlval3  39790  cdlemc  39800  cdlemd9  39809  cdlemd  39810  cdleme21j  39939  cdleme21  39940  cdleme29ex  39977  cdlemefr27cl  40006  cdlemefs27cl  40016  cdleme32d  40047  cdleme32f  40049  cdleme35h2  40060  cdleme40m  40070  cdleme17d3  40099  cdleme48fvg  40103  cdlemeg46fvcl  40109  cdlemeg46fgN  40137  cdleme48fgv  40141  cdleme50trn3  40156  cdlemb3  40209  cdlemg8  40234  cdlemg11a  40240  cdlemg15a  40258  cdlemg15  40259  cdlemg16  40260  cdlemg16z  40262  cdlemg17dN  40266  cdlemg24  40291  cdlemg37  40292  cdlemg29  40308  cdlemg33b  40310  cdlemg38  40318  cdlemg40  40320  trlco  40330  cdlemg44b  40335  ltrncom  40341  trljco  40343  tendococl  40375  tendoplcl  40384  tendoplcom  40385  cdlemj2  40425  tendoid0  40428  tendo1ne0  40431  cdlemk25-3  40507  cdlemk36  40516  cdlemkid4  40537  cdlemk19x  40546  cdlemk53  40560  cdlemk56  40574  cdleml5N  40583  tendospcanN  40626  cdlemm10N  40721  dihord6apre  40859  dihord  40867  dihmeetlem1N  40893  dihglblem2N  40897  dihmeetlem2N  40902  dihmeetbN  40906  dihmeetlem5  40911  dihmeetlem6  40912  dihmeetlem7N  40913  dihmeetlem10N  40919  dihmeetlem12N  40921  dihmeetlem16N  40925  dihmeetlem17N  40926  dihmeetlem18N  40927  dihmeetALTN  40930  dihlspsnssN  40935  dvh3dim2  41051  dvh3dim3N  41052  lcfrlem16  41161  mapdrvallem2  41248  mapdh8ad  41382  hgmapvvlem3  41528  sticksstones1  41749  sticksstones2  41750  aks6d1c6isolem1  41777  resubcan2  42078  diophrw  42321  eldioph2lem1  42322  diophrex  42337  rencldnfi  42383  pellexlem2  42392  pellqrexplicit  42439  infmrgelbi  42440  pellfundglb  42447  pellfund14gap  42449  rmxycomplete  42480  congadd  42529  acongeq  42546  jm2.19  42556  jm2.23  42559  jm2.20nn  42560  jm2.27  42571  jm3.1  42583  lnmepi  42651  lmhmlnmsplit  42653  hbtlem2  42690  dgraa0p  42715  proot1hash  42765  iocunico  42781  iocinico  42782  oasubex  42857  cantnf2  42896  onmcl  42902  omcl2  42904  nadd2rabex  42957  nadd1rabtr  42959  nadd1rabex  42961  fzunt  43027  relexpxpmin  43289  ntrclsk3  43642  grur1cld  43811  ismnu  43840  grumnudlem  43864  ismnushort  43880  rfcnnnub  44540  uzwo4  44559  wessf1ornlem  44697  supxrge  44858  infleinflem2  44891  iccintsng  45046  climsuse  45134  lptre2pt  45166  limcleqr  45170  0ellimcdiv  45175  fnlimfvre  45200  dvnprodlem1  45472  volioc  45498  stoweidlem17  45543  stoweidlem19  45545  stoweidlem20  45546  stoweidlem22  45548  stoweidlem28  45554  stoweidlem34  45560  stoweidlem44  45570  stoweidlem60  45586  wallispilem3  45593  fourierdlem42  45675  fourierdlem48  45680  fourierdlem51  45683  fourierdlem54  45686  fourierdlem74  45706  fourierdlem77  45709  fourierdlem87  45719  fourierdlem97  45729  ioorrnopnlem  45830  ovnsubaddlem2  46097  smfinflem  46343  fsupdm  46368  finfdm  46372  eluzge0nn0  46830  fzopredsuc  46841  imasetpreimafvbijlemfv  46879  lighneallem4  47087  oexpnegALTV  47154  oexpnegnz  47155  tgblthelfgott  47292  rmsupp0  47618  rmsuppss  47620  lincresunit3lem3  47728  lincresunit3lem2  47734  lindssnlvec  47740  fdivmptf  47800  refdivmptf  47801  elbigolo1  47816  rrx2linest  48001  itsclc0lem1  48015  itsclc0lem2  48016  itsclc0yqsollem1  48021  itsclc0b  48031