Theorem simpl1 1192

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl1	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simpl1

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜑)
2	1	3ad2antl1 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:  simpl11  1249  simpl21  1252  simpl31  1255  simp1l1  1267  simp2l1  1273  simp3l1  1279  3anandirs  1474  rspc3ev  3639  2nreu  4444  predtrss  6343  frpomin  6361  f1prex  7304  cocan1  7311  weniso  7374  frrlem4  8314  frrlem10  8320  fprlem1  8325  smogt  8407  smocdmdom  8408  omeulem1  8620  nnmord  8670  nnmword  8671  naddasslem1  8732  naddasslem2  8733  difsnen  9093  enfixsn  9121  mapunen  9186  ac6sfi  9320  fipreima  9398  elfiun  9470  ordiso2  9555  wemaplem2  9587  en2eqpr  10047  indcardi  10081  fodomfi2  10100  iunfictbso  10154  infmap2  10257  cofsmo  10309  cfsmolem  10310  coftr  10313  fin23lem11  10357  fincssdom  10363  fin23lem26  10365  isf32lem9  10401  ac6num  10519  gchdomtri  10669  gchpwdom  10710  winainflem  10733  tskuni  10823  gruima  10842  gruf  10851  grudomon  10857  elnpi  11028  distrlem4pr  11066  prlem934  11073  addcan  11445  addcan2  11446  divmulass  11945  divmulasscom  11946  ltmul1a  12116  suprleub  12234  supmul1  12237  suprzcl  12698  uzsupss  12982  xleadd1a  13295  xlesubadd  13305  xmulasslem3  13328  xlemul2a  13331  xadddilem  13336  xadddi2  13339  ixxun  13403  icoshftf1o  13514  ioounsn  13517  snunioc  13520  lincmb01cmp  13535  iccf1o  13536  nn0p1elfzo  13742  fzofzim  13749  fzoopth  13801  ltexp2a  14206  leexp2  14211  ltexp2r  14213  exple1  14216  expnlbnd2  14273  fun2dmnop0  14543  ccatass  14626  swrdswrdlem  14742  ccatopth  14754  repswpfx  14823  2cshw  14851  cshimadifsn  14868  cshimadifsn0  14869  cshco  14875  repsco  14879  s2f1o  14955  limsupgre  15517  addcn2  15630  mulcn2  15632  ntrivcvgmul  15938  binomrisefac  16078  dvdsmodexp  16298  dvdsadd2b  16343  dvdsexp2im  16364  dvdsmod  16366  oexpneg  16382  sadass  16508  gcdass  16584  rplpwr  16595  lcmfunsnlem1  16674  coprmdvds2  16691  rpmulgcd2  16693  qredeq  16694  rpdvds  16697  cncongr2  16705  rpexp  16759  prmdiveq  16823  hashgcdlem  16825  odzdvds  16833  modprmn0modprm0  16845  coprimeprodsq2  16847  pythagtriplem3  16856  pcdvdsb  16907  pcgcd1  16915  qexpz  16939  pockthg  16944  vdwnnlem1  17033  0ram  17058  ramz2  17062  lubss  18558  lubun  18560  clatleglb  18563  clatglbss  18564  mrelatglb  18605  isnsgrp  18736  issubmnd  18774  ress0g  18775  mhmvlin  18814  gsumccat  18854  frmdss2  18876  submefmnd  18908  mulgneg  19110  mulgdirlem  19123  submmulg  19136  subgmulg  19158  nmzsubg  19183  ghmmulg  19246  gsmsymgreqlem1  19448  pmtrfb  19483  psgnunilem4  19515  odmodnn0  19558  odnncl  19563  odmod  19564  odmulgid  19572  odmulgeq  19575  odf1o1  19590  odf1o2  19591  odngen  19595  gexdvdsi  19601  pgpfi1  19613  odcau  19622  subgslw  19634  fislw  19643  lsmssv  19661  lsmless1x  19662  lsmless2x  19663  lsmsubm  19671  lsmmod  19693  lsmmod2  19694  efgred  19766  cntzcmn  19858  ghmplusg  19864  odadd1  19866  odadd2  19867  odadd  19868  lsmcomx  19874  gsumconst  19952  ablsimpgprmd  20135  srg1zr  20212  ring1eq0  20295  mulgass2  20306  rngisom1  20466  rhmdvdsr  20508  isabvd  20813  rmodislmodlem  20927  rmodislmod  20928  lssintcl  20962  0lmhm  21039  lmhmvsca  21044  reslmhm2b  21053  pwssplit1  21058  pwssplit3  21060  lspfixed  21130  lspsnat  21147  rnglidlrng  21257  2idlcpblrng  21281  lidldvgen  21344  xrsdsreclblem  21430  regsumsupp  21640  obselocv  21748  uvcresum  21813  frlmsslsp  21816  frlmup4  21821  lindff1  21840  f1lindf  21842  lsslindf  21850  islindf4  21858  lbslcic  21861  issubassa  21887  evlsval2  22111  psrplusgpropd  22237  coe1subfv  22269  coe1mul2  22272  mpomatmul  22452  mamutpos  22464  scmatscmide  22513  mavmulsolcl  22557  marrepcl  22570  mdetdiag  22605  mdetunilem1  22618  mdetunilem3  22620  mdetunilem7  22624  mdetunilem9  22626  mdetmul  22629  slesolinvbi  22687  m2pmfzmap  22753  pmatcollpwlem  22786  pmatcollpw  22787  mp2pm2mplem4  22815  chpdmatlem3  22846  chfacfisfcpmat  22861  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmidpmatlem2  22877  cpmadugsumlemB  22880  cpmadugsumlemC  22881  cpmadugsumlemF  22882  riinopn  22914  neiint  23112  topssnei  23132  restntr  23190  iscnp4  23271  cnconst2  23291  cnrest2  23294  cnprest2  23298  cnpdis  23301  cnt0  23354  cnt1  23358  cnhaus  23362  ordthauslem  23391  cncmp  23400  fiuncmp  23412  sscmp  23413  hauscmp  23415  cnconn  23430  unconn  23437  nlly2i  23484  llynlly  23485  nllyidm  23497  finlocfin  23528  ptrescn  23647  xkococnlem  23667  qtopss  23723  kqfvima  23738  r0cld  23746  ordthmeolem  23809  fbssint  23846  fmf  23953  fmss  23954  elfm  23955  rnelfmlem  23960  rnelfm  23961  fmco  23969  flimss2  23980  flimss1  23981  flimrest  23991  flftg  24004  cnpflf2  24008  cnpflf  24009  flfcnp  24012  supnfcls  24028  fclsss1  24030  fclsss2  24031  fcfnei  24043  fcfelbas  24044  cnpfcfi  24048  subgntr  24115  opnsubg  24116  cldsubg  24119  ghmcnp  24123  utop2nei  24259  neipcfilu  24305  bldisj  24408  blgt0  24409  bl2in  24410  blss2ps  24413  blss2  24414  blssps  24434  blss  24435  xmetresbl  24447  lpbl  24516  blcld  24518  stdbdbl  24530  metcnp3  24553  metcnp2  24555  txmetcnp  24560  blval2  24575  nmoix  24750  nmoeq0  24757  icoopnst  24969  iocopnst  24970  xrhmeo  24977  nmhmcn  25153  cphsqrtcl2  25220  cphsqrtcl3  25221  cfil3i  25303  caublcls  25343  bcthlem5  25362  cmetcusp1  25387  cssbn  25409  rrxcph  25426  pjth  25473  ovoliunlem2  25538  volun  25580  volsup2  25640  mbfimaopn2  25692  iblconst  25853  itgconst  25854  dvcnp2  25955  dvcnp2OLD  25956  dvcn  25957  deg1mul3le  26156  deg1tmle  26157  dvdsq1p  26202  ig1peu  26214  ig1pdvds  26219  coeid3  26279  dgrmulc  26311  efcvx  26493  tanord  26580  logdivlti  26662  logccv  26705  recxpcl  26717  cxpeq  26800  ang180  26857  isosctrlem2  26862  cxp2lim  27020  amgm  27034  muval1  27176  dvdssqf  27181  mumullem2  27223  mumul  27224  bcmono  27321  lgsfcl2  27347  lgsdilem  27368  lgsdirprm  27375  lgsdir  27376  lgsdi  27378  lgsne0  27379  padicabv  27674  nosep1o  27726  nosep2o  27727  nosepssdm  27731  nolt02olem  27739  nosupres  27752  nosupbnd1lem1  27753  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  nosupbnd2  27761  noinfres  27767  noinfbnd1lem1  27768  noinfbnd1lem4  27771  noinfbnd1lem6  27773  noinfbnd2  27776  noetasuplem3  27780  noetalem1  27786  scutbdaybnd  27860  sltlpss  27945  slelss  27946  coinitsslt  27953  addsass  28038  addsdi  28181  mulsass  28192  norecdiv  28216  brbtwn2  28920  colinearalglem1  28921  colinearalg  28925  axcgrtr  28930  axsegconlem8  28939  axsegconlem9  28940  axsegconlem10  28941  axcontlem8  28986  axcontlem10  28988  elntg2  29000  vtxdlfuhgr1v  29497  umgr2wlk  29969  erclwwlksym  30040  clwwlkfo  30069  clwwlkext2edg  30075  erclwwlknsym  30089  clwwlknon1  30116  numclwwlk2lem1  30395  numclwwlk5  30407  frgrregord13  30415  nvmul0or  30669  ipval2lem2  30723  lnomul  30779  shless  31378  shlej1  31379  pjspansn  31596  hoadddi  31822  kbmul  31974  homco2  31996  kbass2  32136  eliccelico  32779  elicoelioo  32780  iocinioc2  32781  iocinif  32783  swrdrn2  32939  xrge0adddir  33023  xrge0npcan  33025  archiabl  33205  ress1r  33238  pidlnz  33404  grplsm0l  33431  intlidl  33448  ssmxidl  33502  pstmfval  33895  fmcncfil  33930  zrhnm  33968  qqhnm  33991  measvunilem  34213  volfiniune  34231  dya2iocnrect  34283  sibfinima  34341  probun  34421  probinc  34423  cndprob01  34437  signstfvp  34586  bnj517  34899  bnj594  34926  pconnpi1  35242  cvmsss2  35279  mrsubcv  35515  msubvrs  35565  br6  35757  br4  35758  cgrcomim  35990  cgrtriv  36003  cgrextend  36009  segconeq  36011  btwntriv2  36013  btwnintr  36020  btwnexch3  36021  btwnouttr2  36023  trisegint  36029  cgrsub  36046  cgrxfr  36056  btwnxfr  36057  lineext  36077  btwnconn1lem13  36100  btwnconn1lem14  36101  btwnconn3  36104  segcon2  36106  brsegle  36109  brsegle2  36110  segletr  36115  segleantisym  36116  seglelin  36117  outsideofeu  36132  lineunray  36148  lineelsb2  36149  ivthALT  36336  weiunpo  36466  weiunso  36467  weiunfr  36468  weiunse  36469  lindsenlbs  37622  areacirc  37720  cocanfo  37726  upixp  37736  ismtyima  37810  rrndstprj2  37838  zerdivemp1x  37954  lsatfixedN  39010  lssat  39017  eqlkr  39100  eqlkr2  39101  lkrlsp  39103  lshpkrlem4  39114  opposet  39182  cvrcon3b  39278  cvrcmp  39284  atlen0  39311  atnle  39318  atlatmstc  39320  cvlatexch3  39339  cvlsupr2  39344  hlsupr2  39389  hlrelat2  39405  cvrexchlem  39421  lnnat  39429  atcvrj2b  39434  atle  39438  atexchcvrN  39442  atbtwn  39448  athgt  39458  3dimlem3  39463  3dim1  39469  1cvratlt  39476  1cvrjat  39477  ps-1  39479  ps-2  39480  3atlem3  39487  3atlem5  39489  3atlem7  39491  llni  39510  llni2  39514  atcvrlln2  39521  llnexatN  39523  llncmp  39524  2llnmat  39526  2at0mat0  39527  lplni  39534  lplnnle2at  39543  2atnelpln  39546  lplnllnneN  39558  llncvrlpln2  39559  2lplnmN  39561  2llnmj  39562  lplncmp  39564  lplnexatN  39565  lplnexllnN  39566  2llnm3N  39571  lvoli  39577  lvoli3  39579  islvol2aN  39594  4atlem0a  39595  4atlem3  39598  4atlem3a  39599  4atlem4a  39601  4atlem4b  39602  4atlem4c  39603  4atlem4d  39604  4atlem10b  39607  4atlem11  39611  4atlem12  39614  lplncvrlvol2  39617  lvolcmp  39619  2lplnmj  39624  islinei  39742  pmapglbx  39771  linepmap  39777  lneq2at  39780  lnjatN  39782  lncvrat  39784  lncmp  39785  2llnma3r  39790  elpaddatriN  39805  elpaddat  39806  paddcom  39815  paddss1  39819  paddss2  39820  paddss12  39821  paddasslem6  39827  paddasslem7  39828  paddasslem8  39829  paddasslem9  39830  paddasslem15  39836  pmodlem2  39849  pmodl42N  39853  pmapjoin  39854  llnmod1i2  39862  2polcon4bN  39920  polcon2bN  39922  poml4N  39955  poml6N  39957  osumcllem1N  39958  osumcllem2N  39959  osumcllem11N  39968  osumclN  39969  pmapojoinN  39970  pexmidlem2N  39973  pexmidlem3N  39974  pexmidlem4N  39975  pexmidlem6N  39977  pexmidlem7N  39978  pl42lem2N  39982  pl42lem3N  39983  pl42lem4N  39984  pl42N  39985  lhpexle2lem  40011  lhpexle3lem  40013  lhpexle3  40014  lhpmcvr3  40027  lhp2at0nle  40037  lhprelat3N  40042  4atex  40078  4atex2  40079  lauteq  40097  lautco  40099  ltrncoidN  40130  ltrneq2  40150  ltrnnidn  40176  ltrnideq  40177  trlnid  40181  ltrnatlw  40185  trlnle  40188  trlval3  40189  trlval4  40190  cdlemc  40199  cdlemd5  40204  cdlemd9  40208  ltrneq3  40210  cdleme0moN  40227  cdleme20  40326  cdleme21j  40338  cdleme21  40339  cdleme27cl  40368  cdlemefrs29bpre0  40398  cdlemefs27cl  40415  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme32d  40446  cdleme32f  40448  cdleme32le  40449  cdleme35h2  40459  cdleme38n  40466  cdleme40m  40469  cdleme41snaw  40478  cdleme42ke  40487  cdleme17d3  40498  cdleme48fvg  40502  cdlemeg46fvcl  40508  cdlemeg46fgN  40536  cdleme48gfv1  40538  cdleme48fgv  40540  cdleme50trn3  40555  trlord  40571  ltrniotavalbN  40586  cdlemb3  40608  cdlemg6c  40622  cdlemg6  40625  cdlemg7N  40628  cdlemg8c  40631  cdlemg8  40633  cdlemg11a  40639  cdlemg11b  40644  cdlemg12e  40649  cdlemg15a  40657  cdlemg15  40658  cdlemg16  40659  cdlemg16z  40661  cdlemg16zz  40662  cdlemg17dN  40665  cdlemg18a  40680  cdlemg20  40687  cdlemg22  40689  cdlemg24  40690  cdlemg37  40691  cdlemg31d  40702  cdlemg29  40707  cdlemg33b  40709  cdlemg33  40713  cdlemg38  40717  cdlemg39  40718  cdlemg40  40719  trlco  40729  trlcone  40730  cdlemg42  40731  cdlemg44b  40734  ltrncom  40740  trljco  40742  tendococl  40774  tendoplcl  40783  tendoplcom  40784  cdlemj2  40824  cdlemj3  40825  tendoid0  40827  tendoconid  40831  tendotr  40832  cdlemk25-3  40906  cdlemk26b-3  40907  cdlemk34  40912  cdlemk36  40915  cdlemk38  40917  cdlemkid4  40936  cdlemk35s-id  40940  cdlemk39s-id  40942  cdlemk19x  40945  cdlemk53  40959  cdlemk55  40963  cdlemk55u  40968  cdlemk39u  40970  cdlemk19u  40972  cdlemk56  40973  tendoex  40977  cdleml3N  40980  cdleml5N  40982  tendospcanN  41025  cdlemm10N  41120  cdlemn11pre  41212  dihord2pre  41227  dihvalcqpre  41237  dihopelvalcpre  41250  dihord6apre  41258  dihord5b  41261  dihord5apre  41264  dihord  41266  dihmeetlem1N  41292  dihglblem5apreN  41293  dihglblem3N  41297  dihmeetlem2N  41301  dihglbcpreN  41302  dihmeetbN  41305  dihmeetlem4preN  41308  dihmeetlem5  41310  dihmeetlem7N  41312  dihmeetlem10N  41318  dihmeetlem11N  41319  dihmeetlem12N  41320  dihmeetlem13N  41321  dihmeetlem15N  41323  dihmeetlem16N  41324  dihmeetlem17N  41325  dihmeetlem18N  41326  dihmeetlem19N  41327  dihmeetALTN  41329  dih1dimatlem0  41330  dihlspsnssN  41334  dihlspsnat  41335  mapdh8ad  41781  hdmap14lem14  41883  hgmapvvlem3  41927  aks6d1c6isolem1  42175  dvdsexpnn  42368  resubcan2  42418  mzprename  42760  eldioph2lem1  42771  lzunuz  42779  rencldnfi  42832  pellexlem2  42841  infmrgelbi  42889  pellfundglb  42896  pellfund14gap  42898  qirropth  42919  rmxycomplete  42929  congadd  42978  acongeq  42995  jm2.19  43005  jm2.23  43008  jm2.20nn  43009  jm2.27  43020  jm3.1  43032  aomclem6  43071  lnmepi  43097  lmhmfgsplit  43098  lmhmlnmsplit  43099  pwssplit4  43101  hbtlem2  43136  hbtlem5  43140  dgraa0p  43161  proot1hash  43207  iocunico  43223  oasubex  43299  oege1  43319  relexpxpmin  43730  brtrclfv2  43740  ntrclsiso  44080  ntrclskb  44082  ntrclsk3  44083  k0004lem3  44162  grur1cld  44251  ismnu  44280  grumnudlem  44304  suprnmpt  45179  wessf1ornlem  45190  projf1o  45202  snunioo1  45525  iccintsng  45536  lptre2pt  45655  limcleqr  45659  fnlimfvre  45689  limsupgtlem  45792  volioc  45987  iblspltprt  45988  stoweidlem19  46034  stoweidlem20  46035  stoweidlem22  46037  stoweidlem28  46043  stoweidlem34  46049  stoweidlem44  46059  stoweidlem60  46075  wallispilem3  46082  fourierdlem41  46163  fourierdlem42  46164  fourierdlem49  46170  fourierdlem51  46172  fourierdlem54  46175  fourierdlem74  46195  fourierdlem97  46218  caratheodorylem2  46542  ovnsubaddlem2  46586  hspmbllem2  46642  smflimmpt  46825  smflimsupmpt  46844  smfliminfmpt  46847  funfocofob  47090  fzopredsuc  47335  imasetpreimafvbijlemfv  47389  iccpartigtl  47410  lighneal  47598  oexpnegALTV  47664  oexpnegnz  47665  tgblthelfgott  47802  clnbgrgrim  47902  uhgrimgrlim  47954  gpgusgralem  48011  lidldomn1  48147  ofaddmndmap  48259  lincdifsn  48341  lincellss  48343  lincresunit3lem3  48391  islindeps2  48400  lindssnlvec  48403  fdivmptf  48462  refdivmptf  48463  rrx2linest  48663  itsclc0yqsollem1  48683  itsclc0b  48693  itsclquadb  48697  itscnhlinecirc02plem3  48705  diag1  49004