Theorem simpl2 1172

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  simpl12  1229  simpl22  1232  simpl32  1235  simp1l2  1247  simp2l2  1253  simp3l2  1259  3anandirs  1451  rspc3ev  3552  2nreu  4277  f1prex  6867  weniso  6932  ofmpteq  7248  tfisi  7391  mposn  7608  smogt  7810  smorndom  7811  omeulem1  8011  nnmord  8061  nnmword  8062  difsnen  8397  enfixsn  8424  mapunen  8484  ac6sfi  8559  ordiso2  8776  wemaplem2  8808  wemapso  8812  wemapso2lem  8813  en2eqpr  9229  acndom  9273  infmap2  9440  cflim2  9485  cfsmolem  9492  coftr  9495  fin23lem26  9547  isf32lem9  9583  fin1a2lem9  9630  fin1a2lem10  9631  gchdomtri  9851  canth4  9869  gchpwdom  9892  gruima  10024  grudomon  10039  prn0  10211  distrlem4pr  10248  prlem934  10255  addcan  10626  addcan2  10627  divmulass  11124  divmulasscom  11125  ltmul1a  11292  supmul1  11413  uzsupss  12157  xaddass  12461  xleadd1a  12465  xlesubadd  12475  xmulass  12499  xlemul2a  12501  xadddilem  12506  xadddi  12507  ixxdisj  12572  ixxun  12573  ixxlb  12579  icoshftf1o  12679  icodisj  12681  ioounsn  12682  lincmb01cmp  12700  iccf1o  12701  elfz1b  12795  ssfzoulel  12949  modmuladd  13099  modaddmulmod  13124  ltexp2a  13348  leexp2  13353  ltexp2r  13355  exple1  13358  expnlbnd2  13413  mulsubdivbinom2  13440  fun2dmnop0  13666  ccatass  13754  ccatopth  13910  ccatopthOLD  13911  swrdccatin12lem2a  13929  repswpfx  14007  repswccat  14008  cshwidxmodr  14031  2cshw  14040  repsco  14067  s2f1o  14143  limsupgle  14698  limsupgre  14702  addcn2  14814  mulcn2  14816  binomrisefac  15259  dvdsval2  15473  dvdsadd2b  15519  dvdsmod  15541  oexpneg  15557  sadass  15683  gcdass  15754  rplpwr  15766  rppwr  15767  lcmass  15817  coprmdvds2  15857  rpmulgcd2  15859  rpdvds  15863  coprmprod  15864  cncongr2  15871  rpexp  15923  prmdiveq  15982  hashgcdlem  15984  odzdvds  15991  coprimeprodsq2  16005  pythagtriplem3  16014  pythagtriplem4  16015  pcdvdsb  16064  vdwnnlem1  16190  0ram  16215  ramz2  16219  ramub1lem1  16221  mremre  16736  mrieqv2d  16771  lubss  17592  lubun  17594  clatleglb  17597  clatglbss  17598  mrelatglb  17655  isnsgrp  17759  issubmnd  17789  gsumccat  17849  frmdss2  17872  nmzsubg  18107  ghmnsgima  18156  gsmsymgreqlem1  18322  psgnunilem4  18390  odmodnn0  18433  odnncl  18438  odmod  18439  oddvds  18440  odeq  18443  odmulgid  18445  odmulgeq  18448  odbezout  18449  odf1o1  18461  odf1o2  18462  odngen  18466  gexdvdsi  18472  pgpfi1  18484  odcau  18493  subgslw  18505  fislw  18514  lsmless1x  18533  lsmless2x  18534  lsmsubm  18542  lsmmod  18562  lsmmod2  18563  efgsfo  18627  odadd1  18727  odadd2  18728  odadd  18729  lsmcomx  18735  prdscmnd  18740  gsumconst  18810  srg1zr  19005  csrgbinom  19022  ring1eq0  19066  mulgass2  19077  cntzsubr  19293  isabvd  19316  rmodislmod  19427  0lmhm  19537  lmhmvsca  19542  reslmhm2b  19551  pwssplit1  19556  pwssplit2  19557  pwssplit3  19558  lbspss  19579  lspsnat  19642  lidldvgen  19752  issubassa  19821  evlsval2  20016  coe1subfv  20140  coe1sclmul  20156  coe1sclmul2  20158  xrsdsreclblem  20296  cssmre  20542  obs2ss  20578  uvcresum  20642  frlmsslsp  20645  frlmup4  20650  lindff1  20669  f1lindf  20671  lsslindf  20679  islindf4  20687  mpomatmul  20762  mamutpos  20774  scmatscmide  20823  mavmulsolcl  20867  mulmarep1gsum2  20890  mdetdiaglem  20914  mdetdiag  20915  mdetunilem1  20928  mdetunilem3  20930  mdetunilem9  20936  maducoeval2  20956  madurid  20960  slesolinvbi  20997  cramerimplem1  20999  cramerlem1  21003  cramer  21007  cpmatel2  21028  m2cpm  21056  m2pmfzmap  21062  m2cpminvid2lem  21069  m2cpminvid2  21070  decpmatmul  21087  pmatcollpw1lem2  21090  pmatcollpw1  21091  pmatcollpw2lem  21092  pmatcollpwfi  21097  pm2mpcl  21112  mply1topmatcl  21120  mp2pm2mplem2  21122  mp2pm2mplem4  21124  mp2pm2mplem5  21125  mp2pm2mp  21126  pm2mpghmlem2  21127  pm2mpghmlem1  21128  chfacfisfcpmat  21170  topssnei  21439  cnconst2  21598  cnpresti  21603  cnprest2  21605  cnpdis  21608  cnt0  21661  cnt1  21665  cnhaus  21669  sscmp  21720  hauscmp  21722  cnconn  21737  unconn  21744  finlocfin  21835  comppfsc  21847  kgen2ss  21870  ptpjopn  21927  prdstopn  21943  ptrescn  21954  qtopss  22030  kqfvima  22045  fbssint  22153  fbasrn  22199  filuni  22200  fmss  22261  rnelfm  22268  fmufil  22274  fmco  22276  flimss2  22287  flimss1  22288  flimrest  22298  cnpflf2  22315  flfcnp  22319  supnfcls  22335  fclsss1  22337  fclsss2  22338  isfcf  22349  subgntr  22421  opnsubg  22422  cldsubg  22425  ghmcnp  22429  ustuqtop1  22556  bldisj  22714  blgt0  22715  bl2in  22716  blss2ps  22719  blss2  22720  blssps  22740  blss  22741  xmetresbl  22753  lpbl  22819  blcld  22821  stdbdmopn  22834  metcnp3  22856  metcnp  22857  metcnp2  22858  txmetcnp  22863  blval2  22878  nmoix  23044  nmoi2  23045  nmotri  23054  metdsge  23163  metdseq0  23168  iocopnst  23250  xrhmeo  23256  nmhmcn  23430  cphsqrtcl2  23496  cphsqrtcl3  23497  cssbn  23684  pjth  23748  ovoliunlem2  23810  volun  23852  mbfimaopn2  23964  iblconst  24124  limcvallem  24175  dvfval  24201  dvcnp2  24223  dvcn  24224  deg1mul3le  24416  deg1tmle  24417  dvdsq1p  24460  ig1peu  24471  ig1pdvds  24476  ply1term  24500  coeid3  24536  dgrmulc  24567  dvply1  24579  aaliou2  24635  efcvx  24743  tanord  24826  eflogeq  24889  logdivlti  24907  logccv  24950  recxpcl  24962  cxplea  24983  cxpeq  25042  ang180  25096  isosctrlem2  25101  cxp2lim  25259  amgm  25273  muval1  25415  dvdssqf  25420  mumullem2  25462  mumul  25463  bcmono  25558  lgsneg  25602  lgsdilem  25605  lgsdirprm  25612  lgsdir  25613  lgsdi  25615  lgsne0  25616  brbtwn2  26397  colinearalglem1  26398  colinearalg  26402  axcgrtr  26407  axsegconlem8  26416  axsegconlem9  26417  axsegconlem10  26418  axcontlem2  26457  axcontlem10  26465  elntg2  26477  ewlkle  27093  crctcshwlkn0lem5  27303  wwlknp  27332  wwlksnext  27384  wwlksnextproplem1  27412  wwlksnextproplem1OLD  27413  wspthsnwspthsnon  27425  clwlkclwwlklem3  27510  erclwwlksym  27539  erclwwlknsym  27597  clwwlknonex2lem2  27639  upgriseupth  27739  eucrct2eupthOLD  27779  eucrct2eupth  27780  3cyclfrgrrn  27823  numclwwlk2lem1lem  27879  numclwwlk1lem2foa  27898  numclwwlk1lem2foaOLD  27899  frgrregord13  27956  nvmul0or  28207  ipval2lem2  28261  lnoadd  28315  lnosub  28316  lnomul  28317  shless  28920  shlej1  28921  kbmul  29516  homco2  29538  kbass2  29678  eliccelico  30255  elicoelioo  30256  iocinioc2  30257  iocinif  30259  difioo  30260  xrge0adddir  30411  xrge0npcan  30413  isarchi2  30480  archiabl  30493  rhmdvdsr  30570  lindssn  30610  pstmfval  30780  fmcncfil  30818  zrhnm  30854  qqhnm  30875  nexple  30912  volfiniune  31134  dya2iocnrect  31184  probinc  31325  cndprob01  31339  signswmnd  31473  bnj517  31804  cvmsss2  32106  cvmlift2lem10  32144  br6  32513  funsseq  32531  fprlem1  32658  nolesgn2o  32699  nosep1o  32707  nosepssdm  32711  nosupres  32728  nosupbnd1lem1  32729  nosupbnd1lem4  32732  nosupbnd1lem5  32733  nosupbnd1lem6  32734  noetalem2  32739  cgrtriv  32984  5segofs  32988  btwnouttr2  33004  btwnxfr  33038  lineext  33058  btwnconn1lem13  33081  brsegle2  33091  nn0prpwlem  33191  lindsenlbs  34328  blbnd  34507  ismtyima  34523  rrndstprj2  34551  ghomdiv  34612  grpokerinj  34613  lsatfixedN  35590  lssat  35597  lshpkrlem4  35694  cvrcon3b  35858  atlen0  35891  atcvreq0  35895  atnle  35898  atlatmstc  35900  atlatle  35901  cvlcvr1  35920  hlsupr2  35968  hlrelat2  35984  cvrexchlem  36000  lnnat  36008  atcvrj2b  36013  3dimlem3  36042  3dim1  36048  1cvrjat  36056  llni  36089  llni2  36093  llnexatN  36102  2llnmat  36105  lplni  36113  2atnelpln  36125  llncvrlpln2  36138  2llnmj  36141  lplnexatN  36144  lplnexllnN  36145  2llnm3N  36150  lvoli  36156  lvoli3  36158  lvolnle3at  36163  islvol2aN  36173  4atlem4a  36180  4atlem4b  36181  4atlem11  36190  lplncvrlvol2  36196  2lplnmj  36203  islinei  36321  linepmap  36356  lnjatN  36361  lncvrat  36363  lncmp  36364  elpaddn0  36381  elpaddatriN  36384  elpaddat  36385  paddcom  36394  paddss2  36399  paddss12  36400  paddasslem4  36404  paddasslem9  36409  paddasslem10  36410  pmodl42N  36432  pmapjoin  36433  llnmod1i2  36441  polcon2bN  36501  pclfinclN  36531  poml4N  36534  poml6N  36536  osumcllem1N  36537  osumcllem2N  36538  osumcllem11N  36547  osumclN  36548  pmapojoinN  36549  pexmidlem2N  36552  pexmidlem3N  36553  pexmidlem4N  36554  pexmidlem6N  36556  pexmidlem7N  36557  pl42lem2N  36561  pl42lem3N  36562  pl42lem4N  36563  pl42N  36564  lhprelat3N  36621  4atex  36657  lauteq  36676  lautco  36678  ltrncoidN  36709  ltrneq2  36729  ltrnideq  36756  trlnle  36767  trlval3  36768  cdlemc  36778  cdlemd9  36787  cdlemd  36788  cdleme21j  36917  cdleme21  36918  cdleme29ex  36955  cdlemefr27cl  36984  cdlemefs27cl  36994  cdleme32d  37025  cdleme32f  37027  cdleme35h2  37038  cdleme40m  37048  cdleme17d3  37077  cdleme48fvg  37081  cdlemeg46fvcl  37087  cdlemeg46fgN  37115  cdleme48fgv  37119  cdleme50trn3  37134  cdlemb3  37187  cdlemg8  37212  cdlemg11a  37218  cdlemg15a  37236  cdlemg15  37237  cdlemg16  37238  cdlemg16z  37240  cdlemg17dN  37244  cdlemg24  37269  cdlemg37  37270  cdlemg29  37286  cdlemg33b  37288  cdlemg38  37296  cdlemg40  37298  trlco  37308  cdlemg44b  37313  ltrncom  37319  trljco  37321  tendococl  37353  tendoplcl  37362  tendoplcom  37363  cdlemj2  37403  tendoid0  37406  tendo1ne0  37409  cdlemk25-3  37485  cdlemk36  37494  cdlemkid4  37515  cdlemk19x  37524  cdlemk53  37538  cdlemk56  37552  cdleml5N  37561  tendospcanN  37604  cdlemm10N  37699  dihord6apre  37837  dihord  37845  dihmeetlem1N  37871  dihglblem2N  37875  dihmeetlem2N  37880  dihmeetbN  37884  dihmeetlem5  37889  dihmeetlem6  37890  dihmeetlem7N  37891  dihmeetlem10N  37897  dihmeetlem12N  37899  dihmeetlem16N  37903  dihmeetlem17N  37904  dihmeetlem18N  37905  dihmeetALTN  37908  dihlspsnssN  37913  dvh3dim2  38029  dvh3dim3N  38030  lcfrlem16  38139  mapdrvallem2  38226  mapdh8ad  38360  hgmapvvlem3  38506  resubcan2  38649  diophrw  38751  eldioph2lem1  38752  diophrex  38768  rencldnfi  38814  pellexlem2  38823  pellqrexplicit  38870  infmrgelbi  38871  pellfundglb  38878  pellfund14gap  38880  rmxycomplete  38910  congadd  38959  acongeq  38976  jm2.19  38986  jm2.23  38989  jm2.20nn  38990  jm2.27  39001  jm3.1  39013  lnmepi  39081  lmhmlnmsplit  39083  hbtlem2  39120  dgraa0p  39145  idomrootle  39191  proot1hash  39196  iocunico  39213  iocinico  39214  relexpxpmin  39425  ntrclsk3  39783  grur1cld  39943  ismnu  39972  grumnudlem  39996  ablsimpgfindlem1  40043  rfcnnnub  40712  uzwo4  40735  wessf1ornlem  40870  supxrge  41036  infleinflem2  41069  iccintsng  41231  climsuse  41321  lptre2pt  41353  limcleqr  41357  0ellimcdiv  41362  fnlimfvre  41387  dvnprodlem1  41662  volioc  41688  stoweidlem17  41734  stoweidlem19  41736  stoweidlem20  41737  stoweidlem22  41739  stoweidlem28  41745  stoweidlem34  41751  stoweidlem44  41761  stoweidlem60  41777  wallispilem3  41784  fourierdlem42  41866  fourierdlem48  41871  fourierdlem51  41874  fourierdlem54  41877  fourierdlem74  41897  fourierdlem77  41900  fourierdlem87  41910  fourierdlem97  41920  ioorrnopnlem  42021  ovnsubaddlem2  42285  smfinflem  42523  eluzge0nn0  42919  fzopredsuc  42930  fzoopth  42934  lighneallem4  43144  oexpnegALTV  43211  oexpnegnz  43212  tgblthelfgott  43349  rmsupp0  43783  rmsuppss  43785  lincresunit3lem3  43897  lincresunit3lem2  43903  lindssnlvec  43909  fdivmptf  43970  refdivmptf  43971  elbigolo1  43986  rrx2linest  44098  itsclc0lem1  44112  itsclc0lem2  44113  itsclc0yqsollem1  44118  itsclc0b  44128