Theorem simpl2 1192

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 1186	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)

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

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 1089

This theorem is referenced by:  simpl12  1249  simpl22  1252  simpl32  1255  simp1l2  1267  simp2l2  1273  simp3l2  1279  3anandirs  1472  rspc3ev  3652  2nreu  4467  f1prex  7320  weniso  7390  ofmpteq  7736  tfisi  7896  mposn  8144  fprlem1  8341  smogt  8423  smocdmdom  8424  omeulem1  8638  nnmord  8688  nnmword  8689  naddasslem1  8750  naddasslem2  8751  difsnen  9119  enfixsn  9147  mapunen  9212  ac6sfi  9348  ordiso2  9584  wemaplem2  9616  wemapso2lem  9621  en2eqpr  10076  acndom  10120  infmap2  10286  cflim2  10332  cfsmolem  10339  coftr  10342  fin23lem26  10394  isf32lem9  10430  fin1a2lem9  10477  fin1a2lem10  10478  gchdomtri  10698  canth4  10716  gchpwdom  10739  gruima  10871  grudomon  10886  prn0  11058  distrlem4pr  11095  prlem934  11102  addcan  11474  addcan2  11475  divmulass  11972  divmulasscom  11973  ltmul1a  12143  supmul1  12264  uzsupss  13005  xaddass  13311  xleadd1a  13315  xlesubadd  13325  xmulass  13349  xlemul2a  13351  xadddilem  13356  xadddi  13357  ixxdisj  13422  ixxun  13423  ixxlb  13429  icoshftf1o  13534  icodisj  13536  ioounsn  13537  lincmb01cmp  13555  iccf1o  13556  elfz1b  13653  ssfzoulel  13810  fzoopth  13812  modmuladd  13964  modaddmulmod  13989  ltexp2a  14216  leexp2  14221  ltexp2r  14223  exple1  14226  expnlbnd2  14283  mulsubdivbinom2  14311  fun2dmnop0  14553  ccatass  14636  ccatopth  14764  pfxccatin12lem2a  14775  repswpfx  14833  repswccat  14834  cshwidxmodr  14852  2cshw  14861  repsco  14889  s2f1o  14965  limsupgle  15523  limsupgre  15527  addcn2  15640  mulcn2  15642  binomrisefac  16090  dvdsval2  16305  dvdsadd2b  16354  dvdsmod  16377  oexpneg  16393  sadass  16517  gcdass  16594  rplpwr  16605  lcmass  16661  coprmdvds2  16701  rpmulgcd2  16703  rpdvds  16707  coprmprod  16708  cncongr2  16715  rpexp  16769  prmdiveq  16833  hashgcdlem  16835  odzdvds  16842  coprimeprodsq2  16856  pythagtriplem3  16865  pythagtriplem4  16866  pcdvdsb  16916  vdwnnlem1  17042  0ram  17067  ramz2  17071  ramub1lem1  17073  mremre  17662  mrieqv2d  17697  lubss  18583  lubun  18585  clatleglb  18588  clatglbss  18589  mrelatglb  18630  isnsgrp  18761  issubmnd  18799  gsumccat  18876  frmdss2  18898  submefmnd  18930  nmzsubg  19205  ghmnsgima  19280  gsmsymgreqlem1  19472  psgnunilem4  19539  odmodnn0  19582  odnncl  19587  odmod  19588  oddvds  19589  odeq  19592  odmulgid  19596  odmulgeq  19599  odbezout  19600  odf1o1  19614  odf1o2  19615  odngen  19619  gexdvdsi  19625  pgpfi1  19637  odcau  19646  subgslw  19658  fislw  19667  lsmless1x  19686  lsmless2x  19687  lsmsubm  19695  lsmmod  19717  lsmmod2  19718  efgsfo  19781  odadd1  19890  odadd2  19891  odadd  19892  lsmcomx  19898  prdscmnd  19903  gsumconst  19976  ablsimpgfindlem1  20151  srg1zr  20242  csrgbinom  20259  ring1eq0  20321  mulgass2  20332  rngisom1  20492  rhmdvdsr  20534  cntzsubrng  20593  cntzsubr  20634  isabvd  20835  rmodislmod  20950  rmodislmodOLD  20951  0lmhm  21062  lmhmvsca  21067  reslmhm2b  21076  pwssplit1  21081  pwssplit2  21082  pwssplit3  21083  lbspss  21104  lspsnat  21170  lidldvgen  21367  xrsdsreclblem  21453  cssmre  21734  obs2ss  21772  uvcresum  21836  frlmsslsp  21839  frlmup4  21844  lindff1  21863  f1lindf  21865  lsslindf  21873  islindf4  21881  issubassa  21910  evlsval2  22134  coe1subfv  22290  coe1sclmul  22306  coe1sclmul2  22308  mpomatmul  22473  mamutpos  22485  scmatscmide  22534  mavmulsolcl  22578  mulmarep1gsum2  22601  mdetdiaglem  22625  mdetdiag  22626  mdetunilem1  22639  mdetunilem3  22641  mdetunilem9  22647  maducoeval2  22667  madurid  22671  slesolinvbi  22708  cramerimplem1  22710  cramerlem1  22714  cramer  22718  cpmatel2  22740  m2cpm  22768  m2pmfzmap  22774  m2cpminvid2lem  22781  m2cpminvid2  22782  decpmatmul  22799  pmatcollpw1lem2  22802  pmatcollpw1  22803  pmatcollpw2lem  22804  pmatcollpwfi  22809  pm2mpcl  22824  mply1topmatcl  22832  mp2pm2mplem2  22834  mp2pm2mplem4  22836  mp2pm2mplem5  22837  mp2pm2mp  22838  pm2mpghmlem2  22839  pm2mpghmlem1  22840  chfacfisfcpmat  22882  topssnei  23153  cnconst2  23312  cnpresti  23317  cnprest2  23319  cnpdis  23322  cnt0  23375  cnt1  23379  cnhaus  23383  sscmp  23434  hauscmp  23436  cnconn  23451  unconn  23458  finlocfin  23549  comppfsc  23561  kgen2ss  23584  ptpjopn  23641  prdstopn  23657  ptrescn  23668  qtopss  23744  kqfvima  23759  fbssint  23867  fbasrn  23913  filuni  23914  fmss  23975  rnelfm  23982  fmufil  23988  fmco  23990  flimss2  24001  flimss1  24002  flimrest  24012  cnpflf2  24029  flfcnp  24033  supnfcls  24049  fclsss1  24051  fclsss2  24052  isfcf  24063  subgntr  24136  opnsubg  24137  cldsubg  24140  ghmcnp  24144  ustuqtop1  24271  bldisj  24429  blgt0  24430  bl2in  24431  blss2ps  24434  blss2  24435  blssps  24455  blss  24456  xmetresbl  24468  lpbl  24537  blcld  24539  stdbdmopn  24552  metcnp3  24574  metcnp  24575  metcnp2  24576  txmetcnp  24581  blval2  24596  nmoix  24771  nmoi2  24772  nmotri  24781  metdsge  24890  metdseq0  24895  iocopnst  24989  xrhmeo  24996  nmhmcn  25172  cphsqrtcl2  25239  cphsqrtcl3  25240  cssbn  25428  pjth  25492  ovoliunlem2  25557  volun  25599  mbfimaopn2  25711  iblconst  25873  limcvallem  25926  dvfval  25952  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  deg1mul3le  26176  deg1tmle  26177  dvdsq1p  26222  idomrootle  26232  ig1peu  26234  ig1pdvds  26239  ply1term  26263  coeid3  26299  dgrmulc  26331  dvply1  26343  aaliou2  26400  efcvx  26511  tanord  26598  eflogeq  26662  logdivlti  26680  logccv  26723  recxpcl  26735  cxplea  26756  cxpeq  26818  ang180  26875  isosctrlem2  26880  cxp2lim  27038  amgm  27052  muval1  27194  dvdssqf  27199  mumullem2  27241  mumul  27242  bcmono  27339  lgsneg  27383  lgsdilem  27386  lgsdirprm  27393  lgsdir  27394  lgsdi  27396  lgsne0  27397  nolesgn2o  27734  nogesgn1o  27736  nosep1o  27744  nosep2o  27745  nosepssdm  27749  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem4  27789  noinfbnd1lem6  27791  noinfbnd2  27794  noetasuplem3  27798  noetainflem3  27802  slelss  27964  cofsslt  27970  coinitsslt  27971  cofcutrtime  27979  addsass  28056  addsdi  28199  mulsass  28210  sltmul2  28215  divsmulw  28236  brbtwn2  28938  colinearalglem1  28939  colinearalg  28943  axcgrtr  28948  axsegconlem8  28957  axsegconlem9  28958  axsegconlem10  28959  axcontlem2  28998  axcontlem10  29006  elntg2  29018  ewlkle  29641  crctcshwlkn0lem5  29847  wwlknp  29876  wwlksnext  29926  wwlksnextproplem1  29942  wspthsnwspthsnon  29949  clwlkclwwlklem3  30033  erclwwlksym  30053  erclwwlknsym  30102  upgriseupth  30239  eucrct2eupth  30277  3cyclfrgrrn  30318  numclwwlk2lem1lem  30374  numclwwlk1lem2foa  30386  frgrregord13  30428  nvmul0or  30682  ipval2lem2  30736  lnoadd  30790  lnosub  30791  lnomul  30792  shless  31391  shlej1  31392  kbmul  31987  homco2  32009  kbass2  32149  eliccelico  32782  elicoelioo  32783  iocinioc2  32784  iocinif  32786  difioo  32787  swrdrn2  32921  swrdrn3  32922  xrge0adddir  33004  xrge0npcan  33006  isarchi2  33165  archiabl  33178  pidlnz  33369  lindssn  33371  ssmxidl  33467  pstmfval  33842  fmcncfil  33877  zrhnm  33915  qqhnm  33936  nexple  33973  volfiniune  34194  dya2iocnrect  34246  probinc  34386  cndprob01  34400  signswmnd  34534  bnj517  34861  cvmsss2  35242  cvmlift2lem10  35280  br6  35719  funsseq  35731  cgrtriv  35966  5segofs  35970  btwnouttr2  35986  btwnxfr  36020  lineext  36040  btwnconn1lem13  36063  brsegle2  36073  nn0prpwlem  36288  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  lindsenlbs  37575  blbnd  37747  ismtyima  37763  rrndstprj2  37791  ghomdiv  37852  grpokerinj  37853  lsatfixedN  38965  lssat  38972  lshpkrlem4  39069  cvrcon3b  39233  atlen0  39266  atcvreq0  39270  atnle  39273  atlatmstc  39275  atlatle  39276  cvlcvr1  39295  hlsupr2  39344  hlrelat2  39360  cvrexchlem  39376  lnnat  39384  atcvrj2b  39389  3dimlem3  39418  3dim1  39424  1cvrjat  39432  llni  39465  llni2  39469  llnexatN  39478  2llnmat  39481  lplni  39489  2atnelpln  39501  llncvrlpln2  39514  2llnmj  39517  lplnexatN  39520  lplnexllnN  39521  2llnm3N  39526  lvoli  39532  lvoli3  39534  lvolnle3at  39539  islvol2aN  39549  4atlem4a  39556  4atlem4b  39557  4atlem11  39566  lplncvrlvol2  39572  2lplnmj  39579  islinei  39697  linepmap  39732  lnjatN  39737  lncvrat  39739  lncmp  39740  elpaddn0  39757  elpaddatriN  39760  elpaddat  39761  paddcom  39770  paddss2  39775  paddss12  39776  paddasslem4  39780  paddasslem9  39785  paddasslem10  39786  pmodl42N  39808  pmapjoin  39809  llnmod1i2  39817  polcon2bN  39877  pclfinclN  39907  poml4N  39910  poml6N  39912  osumcllem1N  39913  osumcllem2N  39914  osumcllem11N  39923  osumclN  39924  pmapojoinN  39925  pexmidlem2N  39928  pexmidlem3N  39929  pexmidlem4N  39930  pexmidlem6N  39932  pexmidlem7N  39933  pl42lem2N  39937  pl42lem3N  39938  pl42lem4N  39939  pl42N  39940  lhprelat3N  39997  4atex  40033  lauteq  40052  lautco  40054  ltrncoidN  40085  ltrneq2  40105  ltrnideq  40132  trlnle  40143  trlval3  40144  cdlemc  40154  cdlemd9  40163  cdlemd  40164  cdleme21j  40293  cdleme21  40294  cdleme29ex  40331  cdlemefr27cl  40360  cdlemefs27cl  40370  cdleme32d  40401  cdleme32f  40403  cdleme35h2  40414  cdleme40m  40424  cdleme17d3  40453  cdleme48fvg  40457  cdlemeg46fvcl  40463  cdlemeg46fgN  40491  cdleme48fgv  40495  cdleme50trn3  40510  cdlemb3  40563  cdlemg8  40588  cdlemg11a  40594  cdlemg15a  40612  cdlemg15  40613  cdlemg16  40614  cdlemg16z  40616  cdlemg17dN  40620  cdlemg24  40645  cdlemg37  40646  cdlemg29  40662  cdlemg33b  40664  cdlemg38  40672  cdlemg40  40674  trlco  40684  cdlemg44b  40689  ltrncom  40695  trljco  40697  tendococl  40729  tendoplcl  40738  tendoplcom  40739  cdlemj2  40779  tendoid0  40782  tendo1ne0  40785  cdlemk25-3  40861  cdlemk36  40870  cdlemkid4  40891  cdlemk19x  40900  cdlemk53  40914  cdlemk56  40928  cdleml5N  40937  tendospcanN  40980  cdlemm10N  41075  dihord6apre  41213  dihord  41221  dihmeetlem1N  41247  dihglblem2N  41251  dihmeetlem2N  41256  dihmeetbN  41260  dihmeetlem5  41265  dihmeetlem6  41266  dihmeetlem7N  41267  dihmeetlem10N  41273  dihmeetlem12N  41275  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem18N  41281  dihmeetALTN  41284  dihlspsnssN  41289  dvh3dim2  41405  dvh3dim3N  41406  lcfrlem16  41515  mapdrvallem2  41602  mapdh8ad  41736  hgmapvvlem3  41882  sticksstones1  42103  sticksstones2  42104  aks6d1c6isolem1  42131  resubcan2  42364  diophrw  42715  eldioph2lem1  42716  diophrex  42731  rencldnfi  42777  pellexlem2  42786  pellqrexplicit  42833  infmrgelbi  42834  pellfundglb  42841  pellfund14gap  42843  rmxycomplete  42874  congadd  42923  acongeq  42940  jm2.19  42950  jm2.23  42953  jm2.20nn  42954  jm2.27  42965  jm3.1  42977  lnmepi  43042  lmhmlnmsplit  43044  hbtlem2  43081  dgraa0p  43106  proot1hash  43156  iocunico  43172  iocinico  43173  oasubex  43248  cantnf2  43287  onmcl  43293  omcl2  43295  nadd2rabex  43348  nadd1rabtr  43350  nadd1rabex  43352  fzunt  43417  relexpxpmin  43679  ntrclsk3  44032  grur1cld  44201  ismnu  44230  grumnudlem  44254  ismnushort  44270  rfcnnnub  44936  uzwo4  44955  wessf1ornlem  45092  supxrge  45253  infleinflem2  45286  iccintsng  45441  climsuse  45529  lptre2pt  45561  limcleqr  45565  0ellimcdiv  45570  fnlimfvre  45595  dvnprodlem1  45867  volioc  45893  stoweidlem17  45938  stoweidlem19  45940  stoweidlem20  45941  stoweidlem22  45943  stoweidlem28  45949  stoweidlem34  45955  stoweidlem44  45965  stoweidlem60  45981  wallispilem3  45988  fourierdlem42  46070  fourierdlem48  46075  fourierdlem51  46078  fourierdlem54  46081  fourierdlem74  46101  fourierdlem77  46104  fourierdlem87  46114  fourierdlem97  46124  ioorrnopnlem  46225  ovnsubaddlem2  46492  smfinflem  46738  fsupdm  46763  finfdm  46767  eluzge0nn0  47227  fzopredsuc  47238  imasetpreimafvbijlemfv  47276  lighneallem4  47484  oexpnegALTV  47551  oexpnegnz  47552  tgblthelfgott  47689  clnbgrgrim  47786  rmsupp0  48093  rmsuppss  48095  lincresunit3lem3  48203  lincresunit3lem2  48209  lindssnlvec  48215  fdivmptf  48275  refdivmptf  48276  elbigolo1  48291  rrx2linest  48476  itsclc0lem1  48490  itsclc0lem2  48491  itsclc0yqsollem1  48496  itsclc0b  48506