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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  simpl11  1249  simpl21  1252  simpl31  1255  simp1l1  1267  simp2l1  1273  simp3l1  1279  3anandirs  1473  rspc3ev  3629  2nreu  4442  predtrss  6324  frpomin  6342  f1prex  7282  cocan1  7289  weniso  7351  frrlem4  8274  frrlem10  8280  fprlem1  8285  smogt  8367  smocdmdom  8368  omeulem1  8582  nnmord  8632  nnmword  8633  naddasslem1  8693  naddasslem2  8694  difsnen  9053  enfixsn  9081  mapunen  9146  ac6sfi  9287  fipreima  9358  elfiun  9425  ordiso2  9510  wemaplem2  9542  en2eqpr  10002  indcardi  10036  fodomfi2  10055  iunfictbso  10109  infmap2  10213  cofsmo  10264  cfsmolem  10265  coftr  10268  fin23lem11  10312  fincssdom  10318  fin23lem26  10320  isf32lem9  10356  ac6num  10474  gchdomtri  10624  gchpwdom  10665  winainflem  10688  tskuni  10778  gruima  10797  gruf  10806  grudomon  10812  elnpi  10983  distrlem4pr  11021  prlem934  11028  addcan  11398  addcan2  11399  divmulass  11895  divmulasscom  11896  ltmul1a  12063  suprleub  12180  supmul1  12183  suprzcl  12642  uzsupss  12924  xleadd1a  13232  xlesubadd  13242  xmulasslem3  13265  xlemul2a  13268  xadddilem  13273  xadddi2  13276  ixxun  13340  icoshftf1o  13451  ioounsn  13454  snunioc  13457  lincmb01cmp  13472  iccf1o  13473  nn0p1elfzo  13675  fzofzim  13679  ltexp2a  14131  leexp2  14136  ltexp2r  14138  exple1  14141  expnlbnd2  14197  fun2dmnop0  14455  ccatass  14538  swrdswrdlem  14654  ccatopth  14666  repswpfx  14735  2cshw  14763  cshimadifsn  14780  cshimadifsn0  14781  cshco  14787  repsco  14791  s2f1o  14867  limsupgre  15425  addcn2  15538  mulcn2  15540  ntrivcvgmul  15848  binomrisefac  15986  dvdsmodexp  16205  dvdsadd2b  16249  dvdsexp2im  16270  dvdsmod  16272  oexpneg  16288  sadass  16412  gcdass  16489  rplpwr  16499  lcmfunsnlem1  16574  coprmdvds2  16591  rpmulgcd2  16593  qredeq  16594  rpdvds  16597  cncongr2  16605  rpexp  16659  prmdiveq  16719  hashgcdlem  16721  odzdvds  16728  modprmn0modprm0  16740  coprimeprodsq2  16742  pythagtriplem3  16751  pcdvdsb  16802  pcgcd1  16810  qexpz  16834  pockthg  16839  vdwnnlem1  16928  0ram  16953  ramz2  16957  lubss  18466  lubun  18468  clatleglb  18471  clatglbss  18472  mrelatglb  18513  isnsgrp  18614  issubmnd  18652  ress0g  18653  gsumccat  18722  frmdss2  18744  submefmnd  18776  mulgneg  18972  mulgdirlem  18985  submmulg  18998  subgmulg  19020  nmzsubg  19045  ghmmulg  19104  gsmsymgreqlem1  19298  pmtrfb  19333  psgnunilem4  19365  odmodnn0  19408  odnncl  19413  odmod  19414  odmulgid  19422  odmulgeq  19425  odf1o1  19440  odf1o2  19441  odngen  19445  gexdvdsi  19451  pgpfi1  19463  odcau  19472  subgslw  19484  fislw  19493  lsmssv  19511  lsmless1x  19512  lsmless2x  19513  lsmsubm  19521  lsmmod  19543  lsmmod2  19544  efgred  19616  cntzcmn  19708  ghmplusg  19714  odadd1  19716  odadd2  19717  odadd  19718  lsmcomx  19724  gsumconst  19802  ablsimpgprmd  19985  srg1zr  20038  ring1eq0  20110  mulgass2  20121  rhmdvdsr  20287  isabvd  20428  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  lssintcl  20575  0lmhm  20651  lmhmvsca  20656  reslmhm2b  20665  pwssplit1  20670  pwssplit3  20672  lspfixed  20741  lspsnat  20758  lidldvgen  20893  xrsdsreclblem  20991  regsumsupp  21175  obselocv  21283  uvcresum  21348  frlmsslsp  21351  frlmup4  21356  lindff1  21375  f1lindf  21377  lsslindf  21385  islindf4  21393  lbslcic  21396  issubassa  21421  evlsval2  21650  psrplusgpropd  21758  coe1subfv  21788  coe1mul2  21791  mhmvlin  21899  mpomatmul  21948  mamutpos  21960  scmatscmide  22009  mavmulsolcl  22053  marrepcl  22066  mdetdiag  22101  mdetunilem1  22114  mdetunilem3  22116  mdetunilem7  22120  mdetunilem9  22122  mdetmul  22125  slesolinvbi  22183  m2pmfzmap  22249  pmatcollpwlem  22282  pmatcollpw  22283  mp2pm2mplem4  22311  chpdmatlem3  22342  chfacfisfcpmat  22357  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  chfacfpmmulgsum2  22367  cayhamlem1  22368  cpmidpmatlem2  22373  cpmadugsumlemB  22376  cpmadugsumlemC  22377  cpmadugsumlemF  22378  riinopn  22410  neiint  22608  topssnei  22628  restntr  22686  iscnp4  22767  cnconst2  22787  cnrest2  22790  cnprest2  22794  cnpdis  22797  cnt0  22850  cnt1  22854  cnhaus  22858  ordthauslem  22887  cncmp  22896  fiuncmp  22908  sscmp  22909  hauscmp  22911  cnconn  22926  unconn  22933  nlly2i  22980  llynlly  22981  nllyidm  22993  finlocfin  23024  ptrescn  23143  xkococnlem  23163  qtopss  23219  kqfvima  23234  r0cld  23242  ordthmeolem  23305  fbssint  23342  fmf  23449  fmss  23450  elfm  23451  rnelfmlem  23456  rnelfm  23457  fmco  23465  flimss2  23476  flimss1  23477  flimrest  23487  flftg  23500  cnpflf2  23504  cnpflf  23505  flfcnp  23508  supnfcls  23524  fclsss1  23526  fclsss2  23527  fcfnei  23539  fcfelbas  23540  cnpfcfi  23544  subgntr  23611  opnsubg  23612  cldsubg  23615  ghmcnp  23619  utop2nei  23755  neipcfilu  23801  bldisj  23904  blgt0  23905  bl2in  23906  blss2ps  23909  blss2  23910  blssps  23930  blss  23931  xmetresbl  23943  lpbl  24012  blcld  24014  stdbdbl  24026  metcnp3  24049  metcnp2  24051  txmetcnp  24056  blval2  24071  nmoix  24246  nmoeq0  24253  icoopnst  24455  iocopnst  24456  xrhmeo  24462  nmhmcn  24636  cphsqrtcl2  24703  cphsqrtcl3  24704  cfil3i  24786  caublcls  24826  bcthlem5  24845  cmetcusp1  24870  cssbn  24892  rrxcph  24909  pjth  24956  ovoliunlem2  25020  volun  25062  volsup2  25122  mbfimaopn2  25174  iblconst  25335  itgconst  25336  dvcnp2  25437  dvcn  25438  deg1mul3le  25634  deg1tmle  25635  dvdsq1p  25678  ig1peu  25689  ig1pdvds  25694  coeid3  25754  dgrmulc  25785  efcvx  25961  tanord  26047  logdivlti  26128  logccv  26171  recxpcl  26183  cxpeq  26265  ang180  26319  isosctrlem2  26324  cxp2lim  26481  amgm  26495  muval1  26637  dvdssqf  26642  mumullem2  26684  mumul  26685  bcmono  26780  lgsfcl2  26806  lgsdilem  26827  lgsdirprm  26834  lgsdir  26835  lgsdi  26837  lgsne0  26838  padicabv  27133  nosep1o  27184  nosep2o  27185  nosepssdm  27189  nolt02olem  27197  nosupres  27210  nosupbnd1lem1  27211  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd1lem6  27216  nosupbnd2  27219  noinfres  27225  noinfbnd1lem1  27226  noinfbnd1lem4  27229  noinfbnd1lem6  27231  noinfbnd2  27234  noetasuplem3  27238  noetalem1  27244  scutbdaybnd  27317  sltlpss  27402  slelss  27403  coinitsslt  27408  addsass  27491  addsdi  27613  mulsass  27624  norecdiv  27641  brbtwn2  28194  colinearalglem1  28195  colinearalg  28199  axcgrtr  28204  axsegconlem8  28213  axsegconlem9  28214  axsegconlem10  28215  axcontlem8  28260  axcontlem10  28262  elntg2  28274  vtxdlfuhgr1v  28767  umgr2wlk  29234  erclwwlksym  29305  clwwlkfo  29334  clwwlkext2edg  29340  erclwwlknsym  29354  clwwlknon1  29381  numclwwlk2lem1  29660  numclwwlk5  29672  frgrregord13  29680  nvmul0or  29934  ipval2lem2  29988  lnomul  30044  shless  30643  shlej1  30644  pjspansn  30861  hoadddi  31087  kbmul  31239  homco2  31261  kbass2  31401  eliccelico  32019  elicoelioo  32020  iocinioc2  32021  iocinif  32023  swrdrn2  32149  xrge0adddir  32224  xrge0npcan  32226  archiabl  32375  ress1r  32414  pidlnz  32519  grplsm0l  32544  intlidl  32567  ssmxidl  32621  pstmfval  32907  fmcncfil  32942  zrhnm  32980  qqhnm  33001  measvunilem  33241  volfiniune  33259  dya2iocnrect  33311  sibfinima  33369  probun  33449  probinc  33451  cndprob01  33465  signstfvp  33613  bnj517  33927  bnj594  33954  pconnpi1  34259  cvmsss2  34296  mrsubcv  34532  msubvrs  34582  br6  34758  br4  34759  cgrcomim  34992  cgrtriv  35005  cgrextend  35011  segconeq  35013  btwntriv2  35015  btwnintr  35022  btwnexch3  35023  btwnouttr2  35025  trisegint  35031  cgrsub  35048  cgrxfr  35058  btwnxfr  35059  lineext  35079  btwnconn1lem13  35102  btwnconn1lem14  35103  btwnconn3  35106  segcon2  35108  brsegle  35111  brsegle2  35112  segletr  35117  segleantisym  35118  seglelin  35119  outsideofeu  35134  lineunray  35150  lineelsb2  35151  gg-dvcnp2  35205  ivthALT  35268  lindsenlbs  36531  areacirc  36629  cocanfo  36635  upixp  36645  ismtyima  36719  rrndstprj2  36747  zerdivemp1x  36863  lsatfixedN  37927  lssat  37934  eqlkr  38017  eqlkr2  38018  lkrlsp  38020  lshpkrlem4  38031  opposet  38099  cvrcon3b  38195  cvrcmp  38201  atlen0  38228  atnle  38235  atlatmstc  38237  cvlatexch3  38256  cvlsupr2  38261  hlsupr2  38306  hlrelat2  38322  cvrexchlem  38338  lnnat  38346  atcvrj2b  38351  atle  38355  atexchcvrN  38359  atbtwn  38365  athgt  38375  3dimlem3  38380  3dim1  38386  1cvratlt  38393  1cvrjat  38394  ps-1  38396  ps-2  38397  3atlem3  38404  3atlem5  38406  3atlem7  38408  llni  38427  llni2  38431  atcvrlln2  38438  llnexatN  38440  llncmp  38441  2llnmat  38443  2at0mat0  38444  lplni  38451  lplnnle2at  38460  2atnelpln  38463  lplnllnneN  38475  llncvrlpln2  38476  2lplnmN  38478  2llnmj  38479  lplncmp  38481  lplnexatN  38482  lplnexllnN  38483  2llnm3N  38488  lvoli  38494  lvoli3  38496  islvol2aN  38511  4atlem0a  38512  4atlem3  38515  4atlem3a  38516  4atlem4a  38518  4atlem4b  38519  4atlem4c  38520  4atlem4d  38521  4atlem10b  38524  4atlem11  38528  4atlem12  38531  lplncvrlvol2  38534  lvolcmp  38536  2lplnmj  38541  islinei  38659  pmapglbx  38688  linepmap  38694  lneq2at  38697  lnjatN  38699  lncvrat  38701  lncmp  38702  2llnma3r  38707  elpaddatriN  38722  elpaddat  38723  paddcom  38732  paddss1  38736  paddss2  38737  paddss12  38738  paddasslem6  38744  paddasslem7  38745  paddasslem8  38746  paddasslem9  38747  paddasslem15  38753  pmodlem2  38766  pmodl42N  38770  pmapjoin  38771  llnmod1i2  38779  2polcon4bN  38837  polcon2bN  38839  poml4N  38872  poml6N  38874  osumcllem1N  38875  osumcllem2N  38876  osumcllem11N  38885  osumclN  38886  pmapojoinN  38887  pexmidlem2N  38890  pexmidlem3N  38891  pexmidlem4N  38892  pexmidlem6N  38894  pexmidlem7N  38895  pl42lem2N  38899  pl42lem3N  38900  pl42lem4N  38901  pl42N  38902  lhpexle2lem  38928  lhpexle3lem  38930  lhpexle3  38931  lhpmcvr3  38944  lhp2at0nle  38954  lhprelat3N  38959  4atex  38995  4atex2  38996  lauteq  39014  lautco  39016  ltrncoidN  39047  ltrneq2  39067  ltrnnidn  39093  ltrnideq  39094  trlnid  39098  ltrnatlw  39102  trlnle  39105  trlval3  39106  trlval4  39107  cdlemc  39116  cdlemd5  39121  cdlemd9  39125  ltrneq3  39127  cdleme0moN  39144  cdleme20  39243  cdleme21j  39255  cdleme21  39256  cdleme27cl  39285  cdlemefrs29bpre0  39315  cdlemefs27cl  39332  cdlemefs32sn1aw  39333  cdleme43fsv1snlem  39339  cdleme32d  39363  cdleme32f  39365  cdleme32le  39366  cdleme35h2  39376  cdleme38n  39383  cdleme40m  39386  cdleme41snaw  39395  cdleme42ke  39404  cdleme17d3  39415  cdleme48fvg  39419  cdlemeg46fvcl  39425  cdlemeg46fgN  39453  cdleme48gfv1  39455  cdleme48fgv  39457  cdleme50trn3  39472  trlord  39488  ltrniotavalbN  39503  cdlemb3  39525  cdlemg6c  39539  cdlemg6  39542  cdlemg7N  39545  cdlemg8c  39548  cdlemg8  39550  cdlemg11a  39556  cdlemg11b  39561  cdlemg12e  39566  cdlemg15a  39574  cdlemg15  39575  cdlemg16  39576  cdlemg16z  39578  cdlemg16zz  39579  cdlemg17dN  39582  cdlemg18a  39597  cdlemg20  39604  cdlemg22  39606  cdlemg24  39607  cdlemg37  39608  cdlemg31d  39619  cdlemg29  39624  cdlemg33b  39626  cdlemg33  39630  cdlemg38  39634  cdlemg39  39635  cdlemg40  39636  trlco  39646  trlcone  39647  cdlemg42  39648  cdlemg44b  39651  ltrncom  39657  trljco  39659  tendococl  39691  tendoplcl  39700  tendoplcom  39701  cdlemj2  39741  cdlemj3  39742  tendoid0  39744  tendoconid  39748  tendotr  39749  cdlemk25-3  39823  cdlemk26b-3  39824  cdlemk34  39829  cdlemk36  39832  cdlemk38  39834  cdlemkid4  39853  cdlemk35s-id  39857  cdlemk39s-id  39859  cdlemk19x  39862  cdlemk53  39876  cdlemk55  39880  cdlemk55u  39885  cdlemk39u  39887  cdlemk19u  39889  cdlemk56  39890  tendoex  39894  cdleml3N  39897  cdleml5N  39899  tendospcanN  39942  cdlemm10N  40037  cdlemn11pre  40129  dihord2pre  40144  dihvalcqpre  40154  dihopelvalcpre  40167  dihord6apre  40175  dihord5b  40178  dihord5apre  40181  dihord  40183  dihmeetlem1N  40209  dihglblem5apreN  40210  dihglblem3N  40214  dihmeetlem2N  40218  dihglbcpreN  40219  dihmeetbN  40222  dihmeetlem4preN  40225  dihmeetlem5  40227  dihmeetlem7N  40229  dihmeetlem10N  40235  dihmeetlem11N  40236  dihmeetlem12N  40237  dihmeetlem13N  40238  dihmeetlem15N  40240  dihmeetlem16N  40241  dihmeetlem17N  40242  dihmeetlem18N  40243  dihmeetlem19N  40244  dihmeetALTN  40246  dih1dimatlem0  40247  dihlspsnssN  40251  dihlspsnat  40252  mapdh8ad  40698  hdmap14lem14  40800  hgmapvvlem3  40844  dvdsexpnn  41279  resubcan2  41309  mzprename  41535  eldioph2lem1  41546  lzunuz  41554  rencldnfi  41607  pellexlem2  41616  infmrgelbi  41664  pellfundglb  41671  pellfund14gap  41673  qirropth  41694  rmxycomplete  41704  congadd  41753  acongeq  41770  jm2.19  41780  jm2.23  41783  jm2.20nn  41784  jm2.27  41795  jm3.1  41807  aomclem6  41849  lnmepi  41875  lmhmfgsplit  41876  lmhmlnmsplit  41877  pwssplit4  41879  hbtlem2  41914  hbtlem5  41918  dgraa0p  41939  proot1hash  41990  iocunico  42008  oasubex  42084  oege1  42104  relexpxpmin  42516  brtrclfv2  42526  ntrclsiso  42866  ntrclskb  42868  ntrclsk3  42869  k0004lem3  42948  grur1cld  43039  ismnu  43068  grumnudlem  43092  suprnmpt  43918  wessf1ornlem  43930  projf1o  43944  snunioo1  44273  iccintsng  44284  lptre2pt  44404  limcleqr  44408  fnlimfvre  44438  limsupgtlem  44541  volioc  44736  iblspltprt  44737  stoweidlem19  44783  stoweidlem20  44784  stoweidlem22  44786  stoweidlem28  44792  stoweidlem34  44798  stoweidlem44  44808  stoweidlem60  44824  wallispilem3  44831  fourierdlem41  44912  fourierdlem42  44913  fourierdlem49  44919  fourierdlem51  44921  fourierdlem54  44924  fourierdlem74  44944  fourierdlem97  44967  caratheodorylem2  45291  ovnsubaddlem2  45335  hspmbllem2  45391  smflimmpt  45574  smflimsupmpt  45593  smfliminfmpt  45596  funfocofob  45834  fzopredsuc  46079  fzoopth  46083  imasetpreimafvbijlemfv  46118  iccpartigtl  46139  lighneal  46327  oexpnegALTV  46393  oexpnegnz  46394  tgblthelfgott  46531  rngisom1  46766  rnglidlrng  46806  2idlcpblrng  46814  lidldomn1  46871  ofaddmndmap  47067  lincdifsn  47153  lincellss  47155  lincresunit3lem3  47203  islindeps2  47212  lindssnlvec  47215  fdivmptf  47275  refdivmptf  47276  rrx2linest  47476  itsclc0yqsollem1  47496  itsclc0b  47506  itsclquadb  47510  itscnhlinecirc02plem3  47518