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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl12  1249  simpl22  1252  simpl32  1255  simp1l2  1267  simp2l2  1273  simp3l2  1279  3anandirs  1472  rspc3ev  3628  2nreu  4441  f1prex  7281  weniso  7350  ofmpteq  7691  tfisi  7847  mposn  8088  fprlem1  8284  smogt  8366  smocdmdom  8367  omeulem1  8581  nnmord  8631  nnmword  8632  naddasslem1  8692  naddasslem2  8693  difsnen  9052  enfixsn  9080  mapunen  9145  ac6sfi  9286  ordiso2  9509  wemaplem2  9541  wemapso2lem  9546  en2eqpr  10001  acndom  10045  infmap2  10212  cflim2  10257  cfsmolem  10264  coftr  10267  fin23lem26  10319  isf32lem9  10355  fin1a2lem9  10402  fin1a2lem10  10403  gchdomtri  10623  canth4  10641  gchpwdom  10664  gruima  10796  grudomon  10811  prn0  10983  distrlem4pr  11020  prlem934  11027  addcan  11397  addcan2  11398  divmulass  11894  divmulasscom  11895  ltmul1a  12062  supmul1  12182  uzsupss  12923  xaddass  13227  xleadd1a  13231  xlesubadd  13241  xmulass  13265  xlemul2a  13267  xadddilem  13272  xadddi  13273  ixxdisj  13338  ixxun  13339  ixxlb  13345  icoshftf1o  13450  icodisj  13452  ioounsn  13453  lincmb01cmp  13471  iccf1o  13472  elfz1b  13569  ssfzoulel  13725  modmuladd  13877  modaddmulmod  13902  ltexp2a  14130  leexp2  14135  ltexp2r  14137  exple1  14140  expnlbnd2  14196  mulsubdivbinom2  14221  fun2dmnop0  14454  ccatass  14537  ccatopth  14665  pfxccatin12lem2a  14676  repswpfx  14734  repswccat  14735  cshwidxmodr  14753  2cshw  14762  repsco  14790  s2f1o  14866  limsupgle  15420  limsupgre  15424  addcn2  15537  mulcn2  15539  binomrisefac  15985  dvdsval2  16199  dvdsadd2b  16248  dvdsmod  16271  oexpneg  16287  sadass  16411  gcdass  16488  rplpwr  16498  lcmass  16550  coprmdvds2  16590  rpmulgcd2  16592  rpdvds  16596  coprmprod  16597  cncongr2  16604  rpexp  16658  prmdiveq  16718  hashgcdlem  16720  odzdvds  16727  coprimeprodsq2  16741  pythagtriplem3  16750  pythagtriplem4  16751  pcdvdsb  16801  vdwnnlem1  16927  0ram  16952  ramz2  16956  ramub1lem1  16958  mremre  17547  mrieqv2d  17582  lubss  18465  lubun  18467  clatleglb  18470  clatglbss  18471  mrelatglb  18512  isnsgrp  18613  issubmnd  18651  gsumccat  18721  frmdss2  18743  submefmnd  18775  nmzsubg  19044  ghmnsgima  19115  gsmsymgreqlem1  19297  psgnunilem4  19364  odmodnn0  19407  odnncl  19412  odmod  19413  oddvds  19414  odeq  19417  odmulgid  19421  odmulgeq  19424  odbezout  19425  odf1o1  19439  odf1o2  19440  odngen  19444  gexdvdsi  19450  pgpfi1  19462  odcau  19471  subgslw  19483  fislw  19492  lsmless1x  19511  lsmless2x  19512  lsmsubm  19520  lsmmod  19542  lsmmod2  19543  efgsfo  19606  odadd1  19715  odadd2  19716  odadd  19717  lsmcomx  19723  prdscmnd  19728  gsumconst  19801  ablsimpgfindlem1  19976  srg1zr  20037  csrgbinom  20054  ring1eq0  20109  mulgass2  20120  rhmdvdsr  20286  cntzsubr  20352  isabvd  20427  rmodislmod  20539  rmodislmodOLD  20540  0lmhm  20650  lmhmvsca  20655  reslmhm2b  20664  pwssplit1  20669  pwssplit2  20670  pwssplit3  20671  lbspss  20692  lspsnat  20757  lidldvgen  20892  xrsdsreclblem  20990  cssmre  21245  obs2ss  21283  uvcresum  21347  frlmsslsp  21350  frlmup4  21355  lindff1  21374  f1lindf  21376  lsslindf  21384  islindf4  21392  issubassa  21420  evlsval2  21649  coe1subfv  21787  coe1sclmul  21803  coe1sclmul2  21805  mpomatmul  21947  mamutpos  21959  scmatscmide  22008  mavmulsolcl  22052  mulmarep1gsum2  22075  mdetdiaglem  22099  mdetdiag  22100  mdetunilem1  22113  mdetunilem3  22115  mdetunilem9  22121  maducoeval2  22141  madurid  22145  slesolinvbi  22182  cramerimplem1  22184  cramerlem1  22188  cramer  22192  cpmatel2  22214  m2cpm  22242  m2pmfzmap  22248  m2cpminvid2lem  22255  m2cpminvid2  22256  decpmatmul  22273  pmatcollpw1lem2  22276  pmatcollpw1  22277  pmatcollpw2lem  22278  pmatcollpwfi  22283  pm2mpcl  22298  mply1topmatcl  22306  mp2pm2mplem2  22308  mp2pm2mplem4  22310  mp2pm2mplem5  22311  mp2pm2mp  22312  pm2mpghmlem2  22313  pm2mpghmlem1  22314  chfacfisfcpmat  22356  topssnei  22627  cnconst2  22786  cnpresti  22791  cnprest2  22793  cnpdis  22796  cnt0  22849  cnt1  22853  cnhaus  22857  sscmp  22908  hauscmp  22910  cnconn  22925  unconn  22932  finlocfin  23023  comppfsc  23035  kgen2ss  23058  ptpjopn  23115  prdstopn  23131  ptrescn  23142  qtopss  23218  kqfvima  23233  fbssint  23341  fbasrn  23387  filuni  23388  fmss  23449  rnelfm  23456  fmufil  23462  fmco  23464  flimss2  23475  flimss1  23476  flimrest  23486  cnpflf2  23503  flfcnp  23507  supnfcls  23523  fclsss1  23525  fclsss2  23526  isfcf  23537  subgntr  23610  opnsubg  23611  cldsubg  23614  ghmcnp  23618  ustuqtop1  23745  bldisj  23903  blgt0  23904  bl2in  23905  blss2ps  23908  blss2  23909  blssps  23929  blss  23930  xmetresbl  23942  lpbl  24011  blcld  24013  stdbdmopn  24026  metcnp3  24048  metcnp  24049  metcnp2  24050  txmetcnp  24055  blval2  24070  nmoix  24245  nmoi2  24246  nmotri  24255  metdsge  24364  metdseq0  24369  iocopnst  24455  xrhmeo  24461  nmhmcn  24635  cphsqrtcl2  24702  cphsqrtcl3  24703  cssbn  24891  pjth  24955  ovoliunlem2  25019  volun  25061  mbfimaopn2  25173  iblconst  25334  limcvallem  25387  dvfval  25413  dvcnp2  25436  dvcn  25437  deg1mul3le  25633  deg1tmle  25634  dvdsq1p  25677  ig1peu  25688  ig1pdvds  25693  ply1term  25717  coeid3  25753  dgrmulc  25784  dvply1  25796  aaliou2  25852  efcvx  25960  tanord  26046  eflogeq  26109  logdivlti  26127  logccv  26170  recxpcl  26182  cxplea  26203  cxpeq  26262  ang180  26316  isosctrlem2  26321  cxp2lim  26478  amgm  26492  muval1  26634  dvdssqf  26639  mumullem2  26681  mumul  26682  bcmono  26777  lgsneg  26821  lgsdilem  26824  lgsdirprm  26831  lgsdir  26832  lgsdi  26834  lgsne0  26835  nolesgn2o  27171  nogesgn1o  27173  nosep1o  27181  nosep2o  27182  nosepssdm  27186  nosupres  27207  nosupbnd1lem1  27208  nosupbnd1lem4  27211  nosupbnd1lem5  27212  nosupbnd1lem6  27213  noinfres  27222  noinfbnd1lem1  27223  noinfbnd1lem4  27226  noinfbnd1lem6  27228  noinfbnd2  27231  noetasuplem3  27235  noetainflem3  27239  cofsslt  27402  coinitsslt  27403  cofcutrtime  27411  addsass  27485  addsdi  27607  mulsass  27618  sltmul2  27620  divsmulw  27637  brbtwn2  28160  colinearalglem1  28161  colinearalg  28165  axcgrtr  28170  axsegconlem8  28179  axsegconlem9  28180  axsegconlem10  28181  axcontlem2  28220  axcontlem10  28228  elntg2  28240  ewlkle  28859  crctcshwlkn0lem5  29065  wwlknp  29094  wwlksnext  29144  wwlksnextproplem1  29160  wspthsnwspthsnon  29167  clwlkclwwlklem3  29251  erclwwlksym  29271  erclwwlknsym  29320  upgriseupth  29457  eucrct2eupth  29495  3cyclfrgrrn  29536  numclwwlk2lem1lem  29592  numclwwlk1lem2foa  29604  frgrregord13  29646  nvmul0or  29898  ipval2lem2  29952  lnoadd  30006  lnosub  30007  lnomul  30008  shless  30607  shlej1  30608  kbmul  31203  homco2  31225  kbass2  31365  eliccelico  31983  elicoelioo  31984  iocinioc2  31985  iocinif  31987  difioo  31988  swrdrn2  32113  swrdrn3  32114  xrge0adddir  32188  xrge0npcan  32190  isarchi2  32326  archiabl  32339  pidlnz  32483  lindssn  32489  ssmxidl  32585  pstmfval  32871  fmcncfil  32906  zrhnm  32944  qqhnm  32965  nexple  33002  volfiniune  33223  dya2iocnrect  33275  probinc  33415  cndprob01  33429  signswmnd  33563  bnj517  33891  cvmsss2  34260  cvmlift2lem10  34298  br6  34722  funsseq  34734  cgrtriv  34969  5segofs  34973  btwnouttr2  34989  btwnxfr  35023  lineext  35043  btwnconn1lem13  35066  brsegle2  35076  gg-dvcnp2  35169  nn0prpwlem  35202  lindsenlbs  36478  blbnd  36650  ismtyima  36666  rrndstprj2  36694  ghomdiv  36755  grpokerinj  36756  lsatfixedN  37874  lssat  37881  lshpkrlem4  37978  cvrcon3b  38142  atlen0  38175  atcvreq0  38179  atnle  38182  atlatmstc  38184  atlatle  38185  cvlcvr1  38204  hlsupr2  38253  hlrelat2  38269  cvrexchlem  38285  lnnat  38293  atcvrj2b  38298  3dimlem3  38327  3dim1  38333  1cvrjat  38341  llni  38374  llni2  38378  llnexatN  38387  2llnmat  38390  lplni  38398  2atnelpln  38410  llncvrlpln2  38423  2llnmj  38426  lplnexatN  38429  lplnexllnN  38430  2llnm3N  38435  lvoli  38441  lvoli3  38443  lvolnle3at  38448  islvol2aN  38458  4atlem4a  38465  4atlem4b  38466  4atlem11  38475  lplncvrlvol2  38481  2lplnmj  38488  islinei  38606  linepmap  38641  lnjatN  38646  lncvrat  38648  lncmp  38649  elpaddn0  38666  elpaddatriN  38669  elpaddat  38670  paddcom  38679  paddss2  38684  paddss12  38685  paddasslem4  38689  paddasslem9  38694  paddasslem10  38695  pmodl42N  38717  pmapjoin  38718  llnmod1i2  38726  polcon2bN  38786  pclfinclN  38816  poml4N  38819  poml6N  38821  osumcllem1N  38822  osumcllem2N  38823  osumcllem11N  38832  osumclN  38833  pmapojoinN  38834  pexmidlem2N  38837  pexmidlem3N  38838  pexmidlem4N  38839  pexmidlem6N  38841  pexmidlem7N  38842  pl42lem2N  38846  pl42lem3N  38847  pl42lem4N  38848  pl42N  38849  lhprelat3N  38906  4atex  38942  lauteq  38961  lautco  38963  ltrncoidN  38994  ltrneq2  39014  ltrnideq  39041  trlnle  39052  trlval3  39053  cdlemc  39063  cdlemd9  39072  cdlemd  39073  cdleme21j  39202  cdleme21  39203  cdleme29ex  39240  cdlemefr27cl  39269  cdlemefs27cl  39279  cdleme32d  39310  cdleme32f  39312  cdleme35h2  39323  cdleme40m  39333  cdleme17d3  39362  cdleme48fvg  39366  cdlemeg46fvcl  39372  cdlemeg46fgN  39400  cdleme48fgv  39404  cdleme50trn3  39419  cdlemb3  39472  cdlemg8  39497  cdlemg11a  39503  cdlemg15a  39521  cdlemg15  39522  cdlemg16  39523  cdlemg16z  39525  cdlemg17dN  39529  cdlemg24  39554  cdlemg37  39555  cdlemg29  39571  cdlemg33b  39573  cdlemg38  39581  cdlemg40  39583  trlco  39593  cdlemg44b  39598  ltrncom  39604  trljco  39606  tendococl  39638  tendoplcl  39647  tendoplcom  39648  cdlemj2  39688  tendoid0  39691  tendo1ne0  39694  cdlemk25-3  39770  cdlemk36  39779  cdlemkid4  39800  cdlemk19x  39809  cdlemk53  39823  cdlemk56  39837  cdleml5N  39846  tendospcanN  39889  cdlemm10N  39984  dihord6apre  40122  dihord  40130  dihmeetlem1N  40156  dihglblem2N  40160  dihmeetlem2N  40165  dihmeetbN  40169  dihmeetlem5  40174  dihmeetlem6  40175  dihmeetlem7N  40176  dihmeetlem10N  40182  dihmeetlem12N  40184  dihmeetlem16N  40188  dihmeetlem17N  40189  dihmeetlem18N  40190  dihmeetALTN  40193  dihlspsnssN  40198  dvh3dim2  40314  dvh3dim3N  40315  lcfrlem16  40424  mapdrvallem2  40511  mapdh8ad  40645  hgmapvvlem3  40791  sticksstones1  40957  sticksstones2  40958  resubcan2  41262  diophrw  41487  eldioph2lem1  41488  diophrex  41503  rencldnfi  41549  pellexlem2  41558  pellqrexplicit  41605  infmrgelbi  41606  pellfundglb  41613  pellfund14gap  41615  rmxycomplete  41646  congadd  41695  acongeq  41712  jm2.19  41722  jm2.23  41725  jm2.20nn  41726  jm2.27  41737  jm3.1  41749  lnmepi  41817  lmhmlnmsplit  41819  hbtlem2  41856  dgraa0p  41881  idomrootle  41927  proot1hash  41932  iocunico  41950  iocinico  41951  oasubex  42026  cantnf2  42065  onmcl  42071  omcl2  42073  nadd2rabex  42126  nadd1rabtr  42128  nadd1rabex  42130  fzunt  42196  relexpxpmin  42458  ntrclsk3  42811  grur1cld  42981  ismnu  43010  grumnudlem  43034  ismnushort  43050  rfcnnnub  43710  uzwo4  43730  wessf1ornlem  43872  supxrge  44038  infleinflem2  44071  iccintsng  44226  climsuse  44314  lptre2pt  44346  limcleqr  44350  0ellimcdiv  44355  fnlimfvre  44380  dvnprodlem1  44652  volioc  44678  stoweidlem17  44723  stoweidlem19  44725  stoweidlem20  44726  stoweidlem22  44728  stoweidlem28  44734  stoweidlem34  44740  stoweidlem44  44750  stoweidlem60  44766  wallispilem3  44773  fourierdlem42  44855  fourierdlem48  44860  fourierdlem51  44863  fourierdlem54  44866  fourierdlem74  44886  fourierdlem77  44889  fourierdlem87  44899  fourierdlem97  44909  ioorrnopnlem  45010  ovnsubaddlem2  45277  smfinflem  45523  fsupdm  45548  finfdm  45552  eluzge0nn0  46010  fzopredsuc  46021  fzoopth  46025  imasetpreimafvbijlemfv  46060  lighneallem4  46268  oexpnegALTV  46335  oexpnegnz  46336  tgblthelfgott  46473  rngisom1  46708  cntzsubrng  46736  rmsupp0  47034  rmsuppss  47036  lincresunit3lem3  47145  lincresunit3lem2  47151  lindssnlvec  47157  fdivmptf  47217  refdivmptf  47218  elbigolo1  47233  rrx2linest  47418  itsclc0lem1  47432  itsclc0lem2  47433  itsclc0yqsollem1  47438  itsclc0b  47448