Theorem simpl2 1194

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  simpl12  1251  simpl22  1254  simpl32  1257  simp1l2  1269  simp2l2  1275  simp3l2  1281  3anandirs  1474  rspc3ev  3541  2nreu  4342  f1prex  7072  weniso  7141  ofmpteq  7468  tfisi  7615  mposn  7849  fprlem1  8019  smogt  8082  smorndom  8083  omeulem1  8288  nnmord  8338  nnmword  8339  difsnen  8705  enfixsn  8732  mapunen  8793  ac6sfi  8893  ordiso2  9109  wemaplem2  9141  wemapso2lem  9146  en2eqpr  9586  acndom  9630  infmap2  9797  cflim2  9842  cfsmolem  9849  coftr  9852  fin23lem26  9904  isf32lem9  9940  fin1a2lem9  9987  fin1a2lem10  9988  gchdomtri  10208  canth4  10226  gchpwdom  10249  gruima  10381  grudomon  10396  prn0  10568  distrlem4pr  10605  prlem934  10612  addcan  10981  addcan2  10982  divmulass  11478  divmulasscom  11479  ltmul1a  11646  supmul1  11766  uzsupss  12501  xaddass  12804  xleadd1a  12808  xlesubadd  12818  xmulass  12842  xlemul2a  12844  xadddilem  12849  xadddi  12850  ixxdisj  12915  ixxun  12916  ixxlb  12922  icoshftf1o  13027  icodisj  13029  ioounsn  13030  lincmb01cmp  13048  iccf1o  13049  elfz1b  13146  ssfzoulel  13301  modmuladd  13451  modaddmulmod  13476  ltexp2a  13701  leexp2  13706  ltexp2r  13708  exple1  13711  expnlbnd2  13766  mulsubdivbinom2  13793  fun2dmnop0  14025  ccatass  14110  ccatopth  14246  pfxccatin12lem2a  14257  repswpfx  14315  repswccat  14316  cshwidxmodr  14334  2cshw  14343  repsco  14370  s2f1o  14446  limsupgle  15003  limsupgre  15007  addcn2  15120  mulcn2  15122  binomrisefac  15567  dvdsval2  15781  dvdsadd2b  15830  dvdsmod  15853  oexpneg  15869  sadass  15993  gcdass  16070  rplpwr  16082  lcmass  16134  coprmdvds2  16174  rpmulgcd2  16176  rpdvds  16180  coprmprod  16181  cncongr2  16188  rpexp  16242  prmdiveq  16302  hashgcdlem  16304  odzdvds  16311  coprimeprodsq2  16325  pythagtriplem3  16334  pythagtriplem4  16335  pcdvdsb  16385  vdwnnlem1  16511  0ram  16536  ramz2  16540  ramub1lem1  16542  mremre  17061  mrieqv2d  17096  lubss  17973  lubun  17975  clatleglb  17978  clatglbss  17979  mrelatglb  18020  isnsgrp  18121  issubmnd  18154  gsumccatOLD  18221  gsumccat  18222  frmdss2  18244  submefmnd  18276  nmzsubg  18535  ghmnsgima  18600  gsmsymgreqlem1  18776  psgnunilem4  18843  odmodnn0  18886  odnncl  18891  odmod  18892  oddvds  18893  odeq  18896  odmulgid  18899  odmulgeq  18902  odbezout  18903  odf1o1  18915  odf1o2  18916  odngen  18920  gexdvdsi  18926  pgpfi1  18938  odcau  18947  subgslw  18959  fislw  18968  lsmless1x  18987  lsmless2x  18988  lsmsubm  18996  lsmmod  19019  lsmmod2  19020  efgsfo  19083  odadd1  19187  odadd2  19188  odadd  19189  lsmcomx  19195  prdscmnd  19200  gsumconst  19273  ablsimpgfindlem1  19448  srg1zr  19498  csrgbinom  19515  ring1eq0  19562  mulgass2  19573  cntzsubr  19787  isabvd  19810  rmodislmod  19921  0lmhm  20031  lmhmvsca  20036  reslmhm2b  20045  pwssplit1  20050  pwssplit2  20051  pwssplit3  20052  lbspss  20073  lspsnat  20136  lidldvgen  20247  xrsdsreclblem  20363  cssmre  20609  obs2ss  20645  uvcresum  20709  frlmsslsp  20712  frlmup4  20717  lindff1  20736  f1lindf  20738  lsslindf  20746  islindf4  20754  issubassa  20782  evlsval2  21001  coe1subfv  21141  coe1sclmul  21157  coe1sclmul2  21159  mpomatmul  21297  mamutpos  21309  scmatscmide  21358  mavmulsolcl  21402  mulmarep1gsum2  21425  mdetdiaglem  21449  mdetdiag  21450  mdetunilem1  21463  mdetunilem3  21465  mdetunilem9  21471  maducoeval2  21491  madurid  21495  slesolinvbi  21532  cramerimplem1  21534  cramerlem1  21538  cramer  21542  cpmatel2  21564  m2cpm  21592  m2pmfzmap  21598  m2cpminvid2lem  21605  m2cpminvid2  21606  decpmatmul  21623  pmatcollpw1lem2  21626  pmatcollpw1  21627  pmatcollpw2lem  21628  pmatcollpwfi  21633  pm2mpcl  21648  mply1topmatcl  21656  mp2pm2mplem2  21658  mp2pm2mplem4  21660  mp2pm2mplem5  21661  mp2pm2mp  21662  pm2mpghmlem2  21663  pm2mpghmlem1  21664  chfacfisfcpmat  21706  topssnei  21975  cnconst2  22134  cnpresti  22139  cnprest2  22141  cnpdis  22144  cnt0  22197  cnt1  22201  cnhaus  22205  sscmp  22256  hauscmp  22258  cnconn  22273  unconn  22280  finlocfin  22371  comppfsc  22383  kgen2ss  22406  ptpjopn  22463  prdstopn  22479  ptrescn  22490  qtopss  22566  kqfvima  22581  fbssint  22689  fbasrn  22735  filuni  22736  fmss  22797  rnelfm  22804  fmufil  22810  fmco  22812  flimss2  22823  flimss1  22824  flimrest  22834  cnpflf2  22851  flfcnp  22855  supnfcls  22871  fclsss1  22873  fclsss2  22874  isfcf  22885  subgntr  22958  opnsubg  22959  cldsubg  22962  ghmcnp  22966  ustuqtop1  23093  bldisj  23250  blgt0  23251  bl2in  23252  blss2ps  23255  blss2  23256  blssps  23276  blss  23277  xmetresbl  23289  lpbl  23355  blcld  23357  stdbdmopn  23370  metcnp3  23392  metcnp  23393  metcnp2  23394  txmetcnp  23399  blval2  23414  nmoix  23581  nmoi2  23582  nmotri  23591  metdsge  23700  metdseq0  23705  iocopnst  23791  xrhmeo  23797  nmhmcn  23971  cphsqrtcl2  24037  cphsqrtcl3  24038  cssbn  24226  pjth  24290  ovoliunlem2  24354  volun  24396  mbfimaopn2  24508  iblconst  24669  limcvallem  24722  dvfval  24748  dvcnp2  24771  dvcn  24772  deg1mul3le  24968  deg1tmle  24969  dvdsq1p  25012  ig1peu  25023  ig1pdvds  25028  ply1term  25052  coeid3  25088  dgrmulc  25119  dvply1  25131  aaliou2  25187  efcvx  25295  tanord  25381  eflogeq  25444  logdivlti  25462  logccv  25505  recxpcl  25517  cxplea  25538  cxpeq  25597  ang180  25651  isosctrlem2  25656  cxp2lim  25813  amgm  25827  muval1  25969  dvdssqf  25974  mumullem2  26016  mumul  26017  bcmono  26112  lgsneg  26156  lgsdilem  26159  lgsdirprm  26166  lgsdir  26167  lgsdi  26169  lgsne0  26170  brbtwn2  26950  colinearalglem1  26951  colinearalg  26955  axcgrtr  26960  axsegconlem8  26969  axsegconlem9  26970  axsegconlem10  26971  axcontlem2  27010  axcontlem10  27018  elntg2  27030  ewlkle  27647  crctcshwlkn0lem5  27852  wwlknp  27881  wwlksnext  27931  wwlksnextproplem1  27947  wspthsnwspthsnon  27954  clwlkclwwlklem3  28038  erclwwlksym  28058  erclwwlknsym  28107  upgriseupth  28244  eucrct2eupth  28282  3cyclfrgrrn  28323  numclwwlk2lem1lem  28379  numclwwlk1lem2foa  28391  frgrregord13  28433  nvmul0or  28685  ipval2lem2  28739  lnoadd  28793  lnosub  28794  lnomul  28795  shless  29394  shlej1  29395  kbmul  29990  homco2  30012  kbass2  30152  eliccelico  30772  elicoelioo  30773  iocinioc2  30774  iocinif  30776  difioo  30777  swrdrn2  30900  swrdrn3  30901  xrge0adddir  30974  xrge0npcan  30976  isarchi2  31112  archiabl  31125  rhmdvdsr  31190  pidlnz  31239  lindssn  31241  ssmxidl  31310  pstmfval  31514  fmcncfil  31549  zrhnm  31585  qqhnm  31606  nexple  31643  volfiniune  31864  dya2iocnrect  31914  probinc  32054  cndprob01  32068  signswmnd  32202  bnj517  32532  cvmsss2  32903  cvmlift2lem10  32941  br6  33394  funsseq  33412  nolesgn2o  33560  nogesgn1o  33562  nosep1o  33570  nosep2o  33571  nosepssdm  33575  nosupres  33596  nosupbnd1lem1  33597  nosupbnd1lem4  33600  nosupbnd1lem5  33601  nosupbnd1lem6  33602  noinfres  33611  noinfbnd1lem1  33612  noinfbnd1lem4  33615  noinfbnd1lem6  33617  noinfbnd2  33620  noetasuplem3  33624  noetainflem3  33628  cofsslt  33774  coinitsslt  33775  cofcutrtime  33779  cgrtriv  33990  5segofs  33994  btwnouttr2  34010  btwnxfr  34044  lineext  34064  btwnconn1lem13  34087  brsegle2  34097  nn0prpwlem  34197  lindsenlbs  35458  blbnd  35631  ismtyima  35647  rrndstprj2  35675  ghomdiv  35736  grpokerinj  35737  lsatfixedN  36709  lssat  36716  lshpkrlem4  36813  cvrcon3b  36977  atlen0  37010  atcvreq0  37014  atnle  37017  atlatmstc  37019  atlatle  37020  cvlcvr1  37039  hlsupr2  37087  hlrelat2  37103  cvrexchlem  37119  lnnat  37127  atcvrj2b  37132  3dimlem3  37161  3dim1  37167  1cvrjat  37175  llni  37208  llni2  37212  llnexatN  37221  2llnmat  37224  lplni  37232  2atnelpln  37244  llncvrlpln2  37257  2llnmj  37260  lplnexatN  37263  lplnexllnN  37264  2llnm3N  37269  lvoli  37275  lvoli3  37277  lvolnle3at  37282  islvol2aN  37292  4atlem4a  37299  4atlem4b  37300  4atlem11  37309  lplncvrlvol2  37315  2lplnmj  37322  islinei  37440  linepmap  37475  lnjatN  37480  lncvrat  37482  lncmp  37483  elpaddn0  37500  elpaddatriN  37503  elpaddat  37504  paddcom  37513  paddss2  37518  paddss12  37519  paddasslem4  37523  paddasslem9  37528  paddasslem10  37529  pmodl42N  37551  pmapjoin  37552  llnmod1i2  37560  polcon2bN  37620  pclfinclN  37650  poml4N  37653  poml6N  37655  osumcllem1N  37656  osumcllem2N  37657  osumcllem11N  37666  osumclN  37667  pmapojoinN  37668  pexmidlem2N  37671  pexmidlem3N  37672  pexmidlem4N  37673  pexmidlem6N  37675  pexmidlem7N  37676  pl42lem2N  37680  pl42lem3N  37681  pl42lem4N  37682  pl42N  37683  lhprelat3N  37740  4atex  37776  lauteq  37795  lautco  37797  ltrncoidN  37828  ltrneq2  37848  ltrnideq  37875  trlnle  37886  trlval3  37887  cdlemc  37897  cdlemd9  37906  cdlemd  37907  cdleme21j  38036  cdleme21  38037  cdleme29ex  38074  cdlemefr27cl  38103  cdlemefs27cl  38113  cdleme32d  38144  cdleme32f  38146  cdleme35h2  38157  cdleme40m  38167  cdleme17d3  38196  cdleme48fvg  38200  cdlemeg46fvcl  38206  cdlemeg46fgN  38234  cdleme48fgv  38238  cdleme50trn3  38253  cdlemb3  38306  cdlemg8  38331  cdlemg11a  38337  cdlemg15a  38355  cdlemg15  38356  cdlemg16  38357  cdlemg16z  38359  cdlemg17dN  38363  cdlemg24  38388  cdlemg37  38389  cdlemg29  38405  cdlemg33b  38407  cdlemg38  38415  cdlemg40  38417  trlco  38427  cdlemg44b  38432  ltrncom  38438  trljco  38440  tendococl  38472  tendoplcl  38481  tendoplcom  38482  cdlemj2  38522  tendoid0  38525  tendo1ne0  38528  cdlemk25-3  38604  cdlemk36  38613  cdlemkid4  38634  cdlemk19x  38643  cdlemk53  38657  cdlemk56  38671  cdleml5N  38680  tendospcanN  38723  cdlemm10N  38818  dihord6apre  38956  dihord  38964  dihmeetlem1N  38990  dihglblem2N  38994  dihmeetlem2N  38999  dihmeetbN  39003  dihmeetlem5  39008  dihmeetlem6  39009  dihmeetlem7N  39010  dihmeetlem10N  39016  dihmeetlem12N  39018  dihmeetlem16N  39022  dihmeetlem17N  39023  dihmeetlem18N  39024  dihmeetALTN  39027  dihlspsnssN  39032  dvh3dim2  39148  dvh3dim3N  39149  lcfrlem16  39258  mapdrvallem2  39345  mapdh8ad  39479  hgmapvvlem3  39625  sticksstones1  39771  sticksstones2  39772  resubcan2  40020  diophrw  40225  eldioph2lem1  40226  diophrex  40241  rencldnfi  40287  pellexlem2  40296  pellqrexplicit  40343  infmrgelbi  40344  pellfundglb  40351  pellfund14gap  40353  rmxycomplete  40383  congadd  40432  acongeq  40449  jm2.19  40459  jm2.23  40462  jm2.20nn  40463  jm2.27  40474  jm3.1  40486  lnmepi  40554  lmhmlnmsplit  40556  hbtlem2  40593  dgraa0p  40618  idomrootle  40664  proot1hash  40669  iocunico  40686  iocinico  40687  relexpxpmin  40943  ntrclsk3  41298  grur1cld  41464  ismnu  41493  grumnudlem  41517  ismnushort  41533  rfcnnnub  42193  uzwo4  42215  wessf1ornlem  42336  supxrge  42491  infleinflem2  42524  iccintsng  42677  climsuse  42767  lptre2pt  42799  limcleqr  42803  0ellimcdiv  42808  fnlimfvre  42833  dvnprodlem1  43105  volioc  43131  stoweidlem17  43176  stoweidlem19  43178  stoweidlem20  43179  stoweidlem22  43181  stoweidlem28  43187  stoweidlem34  43193  stoweidlem44  43203  stoweidlem60  43219  wallispilem3  43226  fourierdlem42  43308  fourierdlem48  43313  fourierdlem51  43316  fourierdlem54  43319  fourierdlem74  43339  fourierdlem77  43342  fourierdlem87  43352  fourierdlem97  43362  ioorrnopnlem  43463  ovnsubaddlem2  43727  smfinflem  43965  eluzge0nn0  44420  fzopredsuc  44431  fzoopth  44435  imasetpreimafvbijlemfv  44470  lighneallem4  44678  oexpnegALTV  44745  oexpnegnz  44746  tgblthelfgott  44883  rmsupp0  45320  rmsuppss  45322  lincresunit3lem3  45431  lincresunit3lem2  45437  lindssnlvec  45443  fdivmptf  45503  refdivmptf  45504  elbigolo1  45519  rrx2linest  45704  itsclc0lem1  45718  itsclc0lem2  45719  itsclc0yqsollem1  45724  itsclc0b  45734