Theorem simpl2 1193

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpl12  1250  simpl22  1253  simpl32  1256  simp1l2  1268  simp2l2  1274  simp3l2  1280  3anandirs  1474  rspc3ev  3592  2nreu  4392  f1prex  7213  weniso  7283  ofmpteq  7628  tfisi  7784  mposn  8028  fprlem1  8225  smogt  8282  smocdmdom  8283  omeulem1  8492  nnmord  8542  nnmword  8543  naddasslem1  8604  naddasslem2  8605  difsnen  8967  enfixsn  8994  mapunen  9054  ac6sfi  9163  ordiso2  9396  wemaplem2  9428  wemapso2lem  9433  en2eqpr  9890  acndom  9934  infmap2  10100  cflim2  10146  cfsmolem  10153  coftr  10156  fin23lem26  10208  isf32lem9  10244  fin1a2lem9  10291  fin1a2lem10  10292  gchdomtri  10512  canth4  10530  gchpwdom  10553  gruima  10685  grudomon  10700  prn0  10872  distrlem4pr  10909  prlem934  10916  addcan  11289  addcan2  11290  divmulass  11791  divmulasscom  11792  ltmul1a  11962  supmul1  12083  uzsupss  12830  xaddass  13140  xleadd1a  13144  xlesubadd  13154  xmulass  13178  xlemul2a  13180  xadddilem  13185  xadddi  13186  ixxdisj  13252  ixxun  13253  ixxlb  13259  icoshftf1o  13366  icodisj  13368  ioounsn  13369  lincmb01cmp  13387  iccf1o  13388  elfz1b  13485  ssfzoulel  13652  fzoopth  13654  modmuladd  13812  modaddmulmod  13837  ltexp2a  14065  leexp2  14070  ltexp2r  14072  exple1  14076  expnlbnd2  14133  mulsubdivbinom2  14161  fun2dmnop0  14403  ccatass  14488  ccatopth  14615  pfxccatin12lem2a  14626  repswpfx  14684  repswccat  14685  cshwidxmodr  14703  2cshw  14712  repsco  14739  s2f1o  14815  limsupgle  15376  limsupgre  15380  addcn2  15493  mulcn2  15495  binomrisefac  15941  dvdsval2  16158  dvdsadd2b  16209  dvdsmod  16232  oexpneg  16248  sadass  16374  gcdass  16450  rplpwr  16461  lcmass  16517  coprmdvds2  16557  rpmulgcd2  16559  rpdvds  16563  coprmprod  16564  cncongr2  16571  rpexp  16625  prmdiveq  16689  hashgcdlem  16691  odzdvds  16699  coprimeprodsq2  16713  pythagtriplem3  16722  pythagtriplem4  16723  pcdvdsb  16773  vdwnnlem1  16899  0ram  16924  ramz2  16928  ramub1lem1  16930  mremre  17498  mrieqv2d  17537  lubss  18411  lubun  18413  clatleglb  18416  clatglbss  18417  mrelatglb  18458  isnsgrp  18623  issubmnd  18661  gsumccat  18741  frmdss2  18763  submefmnd  18795  nmzsubg  19070  ghmnsgima  19145  gsmsymgreqlem1  19335  psgnunilem4  19402  odmodnn0  19445  odnncl  19450  odmod  19451  oddvds  19452  odeq  19455  odmulgid  19459  odmulgeq  19462  odbezout  19463  odf1o1  19477  odf1o2  19478  odngen  19482  gexdvdsi  19488  pgpfi1  19500  odcau  19509  subgslw  19521  fislw  19530  lsmless1x  19549  lsmless2x  19550  lsmsubm  19558  lsmmod  19580  lsmmod2  19581  efgsfo  19644  odadd1  19753  odadd2  19754  odadd  19755  lsmcomx  19761  prdscmnd  19766  gsumconst  19839  ablsimpgfindlem1  20014  srg1zr  20126  csrgbinom  20143  ring1eq0  20209  mulgass2  20220  rngisom1  20377  rhmdvdsr  20416  cntzsubrng  20475  cntzsubr  20514  isabvd  20720  rmodislmod  20856  0lmhm  20967  lmhmvsca  20972  reslmhm2b  20981  pwssplit1  20986  pwssplit2  20987  pwssplit3  20988  lbspss  21009  lspsnat  21075  lidldvgen  21264  xrsdsreclblem  21342  cssmre  21623  obs2ss  21659  uvcresum  21723  frlmsslsp  21726  frlmup4  21731  lindff1  21750  f1lindf  21752  lsslindf  21760  islindf4  21768  issubassa  21797  evlsval2  22015  coe1subfv  22173  coe1sclmul  22189  coe1sclmul2  22191  mpomatmul  22354  mamutpos  22366  scmatscmide  22415  mavmulsolcl  22459  mulmarep1gsum2  22482  mdetdiaglem  22506  mdetdiag  22507  mdetunilem1  22520  mdetunilem3  22522  mdetunilem9  22528  maducoeval2  22548  madurid  22552  slesolinvbi  22589  cramerimplem1  22591  cramerlem1  22595  cramer  22599  cpmatel2  22621  m2cpm  22649  m2pmfzmap  22655  m2cpminvid2lem  22662  m2cpminvid2  22663  decpmatmul  22680  pmatcollpw1lem2  22683  pmatcollpw1  22684  pmatcollpw2lem  22685  pmatcollpwfi  22690  pm2mpcl  22705  mply1topmatcl  22713  mp2pm2mplem2  22715  mp2pm2mplem4  22717  mp2pm2mplem5  22718  mp2pm2mp  22719  pm2mpghmlem2  22720  pm2mpghmlem1  22721  chfacfisfcpmat  22763  topssnei  23032  cnconst2  23191  cnpresti  23196  cnprest2  23198  cnpdis  23201  cnt0  23254  cnt1  23258  cnhaus  23262  sscmp  23313  hauscmp  23315  cnconn  23330  unconn  23337  finlocfin  23428  comppfsc  23440  kgen2ss  23463  ptpjopn  23520  prdstopn  23536  ptrescn  23547  qtopss  23623  kqfvima  23638  fbssint  23746  fbasrn  23792  filuni  23793  fmss  23854  rnelfm  23861  fmufil  23867  fmco  23869  flimss2  23880  flimss1  23881  flimrest  23891  cnpflf2  23908  flfcnp  23912  supnfcls  23928  fclsss1  23930  fclsss2  23931  isfcf  23942  subgntr  24015  opnsubg  24016  cldsubg  24019  ghmcnp  24023  ustuqtop1  24149  bldisj  24306  blgt0  24307  bl2in  24308  blss2ps  24311  blss2  24312  blssps  24332  blss  24333  xmetresbl  24345  lpbl  24411  blcld  24413  stdbdmopn  24426  metcnp3  24448  metcnp  24449  metcnp2  24450  txmetcnp  24455  blval2  24470  nmoix  24637  nmoi2  24638  nmotri  24647  metdsge  24758  metdseq0  24763  iocopnst  24857  xrhmeo  24864  nmhmcn  25040  cphsqrtcl2  25106  cphsqrtcl3  25107  cssbn  25295  pjth  25359  ovoliunlem2  25424  volun  25466  mbfimaopn2  25578  iblconst  25739  limcvallem  25792  dvfval  25818  dvcnp2  25841  dvcnp2OLD  25842  dvcn  25843  deg1mul3le  26042  deg1tmle  26043  dvdsq1p  26088  idomrootle  26098  ig1peu  26100  ig1pdvds  26105  ply1term  26129  coeid3  26165  dgrmulc  26197  dvply1  26211  aaliou2  26268  efcvx  26379  tanord  26467  eflogeq  26531  logdivlti  26549  logccv  26592  recxpcl  26604  cxplea  26625  cxpeq  26687  ang180  26744  isosctrlem2  26749  cxp2lim  26907  amgm  26921  muval1  27063  dvdssqf  27068  mumullem2  27110  mumul  27111  bcmono  27208  lgsneg  27252  lgsdilem  27255  lgsdirprm  27262  lgsdir  27263  lgsdi  27265  lgsne0  27266  nolesgn2o  27603  nogesgn1o  27605  nosep1o  27613  nosep2o  27614  nosepssdm  27618  nosupres  27639  nosupbnd1lem1  27640  nosupbnd1lem4  27643  nosupbnd1lem5  27644  nosupbnd1lem6  27645  noinfres  27654  noinfbnd1lem1  27655  noinfbnd1lem4  27658  noinfbnd1lem6  27660  noinfbnd2  27663  noetasuplem3  27667  noetainflem3  27671  slelss  27847  cofsslt  27855  coinitsslt  27856  cofcutrtime  27864  addsass  27941  addsdi  28087  mulsass  28098  sltmul2  28103  divsmulw  28125  brbtwn2  28876  colinearalglem1  28877  colinearalg  28881  axcgrtr  28886  axsegconlem8  28895  axsegconlem9  28896  axsegconlem10  28897  axcontlem2  28936  axcontlem10  28944  elntg2  28956  ewlkle  29577  crctcshwlkn0lem5  29785  wwlknp  29814  wwlksnext  29864  wwlksnextproplem1  29880  wspthsnwspthsnon  29887  clwlkclwwlklem3  29971  erclwwlksym  29991  erclwwlknsym  30040  upgriseupth  30177  eucrct2eupth  30215  3cyclfrgrrn  30256  numclwwlk2lem1lem  30312  numclwwlk1lem2foa  30324  frgrregord13  30366  nvmul0or  30620  ipval2lem2  30674  lnoadd  30728  lnosub  30729  lnomul  30730  shless  31329  shlej1  31330  kbmul  31925  homco2  31947  kbass2  32087  eliccelico  32750  elicoelioo  32751  iocinioc2  32752  iocinif  32754  difioo  32755  nexple  32817  swrdrn2  32925  swrdrn3  32926  xrge0adddir  32989  xrge0npcan  32991  isarchi2  33144  archiabl  33157  pidlnz  33331  lindssn  33333  ssmxidl  33429  pstmfval  33899  fmcncfil  33934  zrhnm  33970  qqhnm  33993  volfiniune  34233  dya2iocnrect  34284  probinc  34424  cndprob01  34438  signswmnd  34560  bnj517  34887  cvmsss2  35286  cvmlift2lem10  35324  br6  35769  funsseq  35780  cgrtriv  36015  5segofs  36019  btwnouttr2  36035  btwnxfr  36069  lineext  36089  btwnconn1lem13  36112  brsegle2  36122  nn0prpwlem  36335  weiunpo  36478  weiunso  36479  weiunfr  36480  weiunse  36481  lindsenlbs  37634  blbnd  37806  ismtyima  37822  rrndstprj2  37850  ghomdiv  37911  grpokerinj  37912  lsatfixedN  39027  lssat  39034  lshpkrlem4  39131  cvrcon3b  39295  atlen0  39328  atcvreq0  39332  atnle  39335  atlatmstc  39337  atlatle  39338  cvlcvr1  39357  hlsupr2  39405  hlrelat2  39421  cvrexchlem  39437  lnnat  39445  atcvrj2b  39450  3dimlem3  39479  3dim1  39485  1cvrjat  39493  llni  39526  llni2  39530  llnexatN  39539  2llnmat  39542  lplni  39550  2atnelpln  39562  llncvrlpln2  39575  2llnmj  39578  lplnexatN  39581  lplnexllnN  39582  2llnm3N  39587  lvoli  39593  lvoli3  39595  lvolnle3at  39600  islvol2aN  39610  4atlem4a  39617  4atlem4b  39618  4atlem11  39627  lplncvrlvol2  39633  2lplnmj  39640  islinei  39758  linepmap  39793  lnjatN  39798  lncvrat  39800  lncmp  39801  elpaddn0  39818  elpaddatriN  39821  elpaddat  39822  paddcom  39831  paddss2  39836  paddss12  39837  paddasslem4  39841  paddasslem9  39846  paddasslem10  39847  pmodl42N  39869  pmapjoin  39870  llnmod1i2  39878  polcon2bN  39938  pclfinclN  39968  poml4N  39971  poml6N  39973  osumcllem1N  39974  osumcllem2N  39975  osumcllem11N  39984  osumclN  39985  pmapojoinN  39986  pexmidlem2N  39989  pexmidlem3N  39990  pexmidlem4N  39991  pexmidlem6N  39993  pexmidlem7N  39994  pl42lem2N  39998  pl42lem3N  39999  pl42lem4N  40000  pl42N  40001  lhprelat3N  40058  4atex  40094  lauteq  40113  lautco  40115  ltrncoidN  40146  ltrneq2  40166  ltrnideq  40193  trlnle  40204  trlval3  40205  cdlemc  40215  cdlemd9  40224  cdlemd  40225  cdleme21j  40354  cdleme21  40355  cdleme29ex  40392  cdlemefr27cl  40421  cdlemefs27cl  40431  cdleme32d  40462  cdleme32f  40464  cdleme35h2  40475  cdleme40m  40485  cdleme17d3  40514  cdleme48fvg  40518  cdlemeg46fvcl  40524  cdlemeg46fgN  40552  cdleme48fgv  40556  cdleme50trn3  40571  cdlemb3  40624  cdlemg8  40649  cdlemg11a  40655  cdlemg15a  40673  cdlemg15  40674  cdlemg16  40675  cdlemg16z  40677  cdlemg17dN  40681  cdlemg24  40706  cdlemg37  40707  cdlemg29  40723  cdlemg33b  40725  cdlemg38  40733  cdlemg40  40735  trlco  40745  cdlemg44b  40750  ltrncom  40756  trljco  40758  tendococl  40790  tendoplcl  40799  tendoplcom  40800  cdlemj2  40840  tendoid0  40843  tendo1ne0  40846  cdlemk25-3  40922  cdlemk36  40931  cdlemkid4  40952  cdlemk19x  40961  cdlemk53  40975  cdlemk56  40989  cdleml5N  40998  tendospcanN  41041  cdlemm10N  41136  dihord6apre  41274  dihord  41282  dihmeetlem1N  41308  dihglblem2N  41312  dihmeetlem2N  41317  dihmeetbN  41321  dihmeetlem5  41326  dihmeetlem6  41327  dihmeetlem7N  41328  dihmeetlem10N  41334  dihmeetlem12N  41336  dihmeetlem16N  41340  dihmeetlem17N  41341  dihmeetlem18N  41342  dihmeetALTN  41345  dihlspsnssN  41350  dvh3dim2  41466  dvh3dim3N  41467  lcfrlem16  41576  mapdrvallem2  41663  mapdh8ad  41797  hgmapvvlem3  41943  sticksstones1  42158  sticksstones2  42159  aks6d1c6isolem1  42186  resubcan2  42400  diophrw  42771  eldioph2lem1  42772  diophrex  42787  rencldnfi  42833  pellexlem2  42842  pellqrexplicit  42889  infmrgelbi  42890  pellfundglb  42897  pellfund14gap  42899  rmxycomplete  42929  congadd  42978  acongeq  42995  jm2.19  43005  jm2.23  43008  jm2.20nn  43009  jm2.27  43020  jm3.1  43032  lnmepi  43097  lmhmlnmsplit  43099  hbtlem2  43136  dgraa0p  43161  proot1hash  43207  iocunico  43223  iocinico  43224  oasubex  43298  cantnf2  43337  onmcl  43343  omcl2  43345  nadd2rabex  43398  nadd1rabtr  43400  nadd1rabex  43402  fzunt  43467  relexpxpmin  43729  ntrclsk3  44082  grur1cld  44244  ismnu  44273  grumnudlem  44297  ismnushort  44313  rfcnnnub  45052  uzwo4  45069  wessf1ornlem  45201  supxrge  45356  infleinflem2  45388  iccintsng  45542  climsuse  45627  lptre2pt  45657  limcleqr  45661  0ellimcdiv  45666  fnlimfvre  45691  dvnprodlem1  45963  volioc  45989  stoweidlem17  46034  stoweidlem19  46036  stoweidlem20  46037  stoweidlem22  46039  stoweidlem28  46045  stoweidlem34  46051  stoweidlem44  46061  stoweidlem60  46077  wallispilem3  46084  fourierdlem42  46166  fourierdlem48  46171  fourierdlem51  46174  fourierdlem54  46177  fourierdlem74  46197  fourierdlem77  46200  fourierdlem87  46210  fourierdlem97  46220  ioorrnopnlem  46321  ovnsubaddlem2  46588  smfinflem  46834  fsupdm  46859  finfdm  46863  eluzge0nn0  47322  fzopredsuc  47333  imasetpreimafvbijlemfv  47412  lighneallem4  47620  oexpnegALTV  47687  oexpnegnz  47688  tgblthelfgott  47825  clnbgrgrim  47944  isubgr3stgrlem3  47978  rmsupp0  48378  rmsuppss  48380  lincresunit3lem3  48485  lincresunit3lem2  48491  lindssnlvec  48497  fdivmptf  48552  refdivmptf  48553  elbigolo1  48568  rrx2linest  48753  itsclc0lem1  48767  itsclc0lem2  48768  itsclc0yqsollem1  48773  itsclc0b  48783  setc1onsubc  49613