Theorem simpl1 1210

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl11  1267  simpl21  1270  simpl31  1273  simp1l1  1285  simp2l1  1291  simp3l1  1297  3anandirs  1502  rspc3ev  3596  2nreu  4405  predtrss  6343  frpomin  6361  f1prex  7315  cocan1  7322  weniso  7387  frrlem4  8335  frrlem10  8341  fprlem1  8346  smogt  8403  smocdmdom  8404  omeulem1  8618  nnmord  8669  nnmword  8670  naddasslem1  8732  naddasslem2  8733  difsnen  9106  enfixsn  9133  mapunen  9193  ac6sfi  9303  fissorduni  9310  fipreima  9375  elfiun  9449  ordiso2  9536  wemaplem2  9568  en2eqpr  10113  indcardi  10147  fodomfi2  10166  iunfictbso  10220  infmap2  10322  cofsmo  10374  cfsmolem  10375  coftr  10378  fin23lem11  10422  fincssdom  10428  fin23lem26  10430  isf32lem9  10466  ac6num  10584  gchdomtri  10741  gchpwdom  10782  winainflem  10805  tskuni  10895  gruima  10914  gruf  10923  grudomon  10929  elnpi  11100  distrlem4pr  11138  prlem934  11145  addcan  11521  addcan2  11522  divmulass  12024  divmulasscom  12025  ltmul1a  12193  suprleub  12310  supmul1  12313  suprzcl  12806  uzsupss  13094  xleadd1a  13410  xlesubadd  13420  xmulasslem3  13443  xlemul2a  13446  xadddilem  13451  xadddi2  13454  ixxun  13519  icoshftf1o  13632  ioounsn  13635  snunioc  13638  lincmb01cmp  13653  iccf1o  13654  nn0p1elfzo  13864  fzofzim  13871  fzoopth  13924  ltexp2a  14336  leexp2  14341  ltexp2r  14343  exple1  14347  expnlbnd2  14405  fun2dmnop0  14676  ccatass  14761  swrdswrdlem  14881  ccatopth  14893  repswpfx  14964  2cshw  14992  cshimadifsn  15008  cshimadifsn0  15009  cshco  15015  repsco  15019  s2f1o  15096  limsupgre  15677  addcn2  15790  mulcn2  15792  ntrivcvgmul  16100  binomrisefac  16237  dvdsmodexp  16459  dvdsadd2b  16505  dvdsexp2im  16526  dvdsmod  16528  oexpneg  16544  sadass  16670  gcdass  16749  rplpwr  16761  dvdsexpnn  16769  lcmfunsnlem1  16841  coprmdvds2  16858  rpmulgcd2  16860  qredeq  16861  rpdvds  16864  cncongr2  16872  rpexp  16927  prmdiveq  16992  hashgcdlem  16994  odzdvds  17002  modprmn0modprm0  17014  coprimeprodsq2  17016  pythagtriplem3  17025  pcdvdsb  17076  pcgcd1  17084  qexpz  17108  pockthg  17113  vdwnnlem1  17202  0ram  17227  ramz2  17231  lubss  18716  lubun  18718  clatleglb  18721  clatglbss  18722  mrelatglb  18763  isnsgrp  18941  issubmnd  18982  ress0gOLD  18984  mhmvlin  19025  gsumccat  19066  frmdss2  19088  submefmnd  19120  mulgneg  19331  mulgdirlem  19344  submmulg  19357  subgmulg  19380  nmzsubg  19404  ghmmulg  19471  gsmsymgreqlem1  19674  pmtrfb  19709  psgnunilem4  19741  odmodnn0  19784  odnncl  19789  odmod  19790  odmulgid  19798  odmulgeq  19801  odf1o1  19816  odf1o2  19817  odngen  19821  gexdvdsi  19827  pgpfi1  19839  odcau  19848  subgslw  19860  fislw  19869  lsmssv  19887  lsmless1x  19888  lsmless2x  19889  lsmsubm  19897  lsmmod  19919  lsmmod2  19920  efgred  19992  cntzcmn  20084  ghmplusg  20090  odadd1  20092  odadd2  20093  odadd  20094  lsmcomx  20100  gsumconst  20178  ablsimpgprmd  20361  ring1eq0  20559  mulgass2  20570  rngisom1  20726  rhmdvdsr  20788  isabvd  21099  rmodislmodlem  21234  rmodislmod  21235  lssintcl  21269  0lmhm  21345  lmhmvsca  21350  reslmhm2b  21359  pwssplit1  21364  pwssplit3  21366  lspfixed  21436  lspsnat  21453  unichnlidl  21546  pidlnz  21558  rnglidlrng  21565  2idlcpblrng  21595  lidldvgen  21688  xrsdsreclblem  21749  regsumsupp  21958  obselocv  22064  uvcresum  22129  frlmsslsp  22132  frlmup4  22137  lindff1  22156  f1lindf  22158  lsslindf  22166  islindf4  22174  lbslcic  22177  lindsenlbs  22187  issubassa  22205  evlsval2  22426  psrplusgpropd  22583  coe1subfv  22615  coe1mul2  22618  mpomatmul  22791  mamutpos  22803  scmatscmide  22852  mavmulsolcl  22896  marrepcl  22909  mdetdiag  22944  mdetunilem1  22957  mdetunilem3  22959  mdetunilem7  22963  mdetunilem9  22965  mdetmul  22968  slesolinvbi  23029  m2pmfzmap  23095  pmatcollpwlem  23128  pmatcollpw  23129  mp2pm2mplem4  23157  chpdmatlem3  23188  chfacfisfcpmat  23203  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  chfacfpmmulgsum2  23213  cayhamlem1  23214  cpmidpmatlem2  23219  cpmadugsumlemB  23222  cpmadugsumlemC  23223  cpmadugsumlemF  23224  riinopn  23256  neiint  23452  topssnei  23472  restntr  23530  iscnp4  23611  cnconst2  23631  cnrest2  23634  cnprest2  23638  cnpdis  23641  cnt0  23694  cnt1  23698  cnhaus  23702  ordthauslem  23731  cncmp  23740  fiuncmp  23752  sscmp  23753  hauscmp  23755  cnconn  23770  unconn  23777  nlly2i  23825  llynlly  23826  nllyidm  23838  finlocfin  23869  ptrescn  23988  xkococnlem  24008  qtopss  24064  kqfvima  24079  r0cld  24087  ordthmeolem  24150  fbssint  24187  fmf  24294  fmss  24295  elfm  24296  rnelfmlem  24301  rnelfm  24302  fmco  24310  flimss2  24321  flimss1  24322  flimrest  24332  flftg  24345  cnpflf2  24349  cnpflf  24350  flfcnp  24353  supnfcls  24369  fclsss1  24371  fclsss2  24372  fcfnei  24384  fcfelbas  24385  cnpfcfi  24389  subgntr  24456  opnsubg  24457  cldsubg  24460  ghmcnp  24464  utop2nei  24599  neipcfilu  24644  bldisj  24747  blgt0  24748  bl2in  24749  blss2ps  24752  blss2  24753  blssps  24773  blss  24774  xmetresbl  24786  lpbl  24852  blcld  24854  stdbdbl  24866  metcnp3  24889  metcnp2  24891  txmetcnp  24896  blval2  24911  nmoix  25078  nmoeq0  25085  icoopnst  25290  iocopnst  25291  xrhmeo  25297  nmhmcn  25471  cphsqrtcl2  25537  cphsqrtcl3  25538  cfil3i  25620  caublcls  25660  bcthlem5  25679  cmetcusp1  25704  cssbn  25726  rrxcph  25743  pjth  25790  ovoliunlem2  25854  volun  25896  volsup2  25956  mbfimaopn2  26008  iblconst  26168  itgconst  26169  dvcnp2  26270  dvcn  26271  deg1mul3le  26465  deg1tmle  26466  dvdsq1p  26511  ig1peu  26523  ig1pdvds  26528  coeid3  26589  dgrmulc  26620  efcvx  26806  tanord  26896  logdivlti  26978  logccv  27021  recxpcl  27033  cxpeq  27115  ang180  27172  isosctrlem2  27177  cxp2lim  27334  amgm  27348  muval1  27490  dvdssqf  27495  mumullem2  27537  mumul  27538  bcmono  27634  lgsfcl2  27660  lgsdilem  27681  lgsdirprm  27688  lgsdir  27689  lgsdi  27691  lgsne0  27692  padicabv  27987  nosep1o  28068  nosep2o  28069  nosepssdm  28073  nolt02olem  28081  nosupres  28094  nosupbnd1lem1  28095  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd1lem6  28100  nosupbnd2  28103  noinfres  28109  noinfbnd1lem1  28110  noinfbnd1lem4  28113  noinfbnd1lem6  28115  noinfbnd2  28118  noetasuplem3  28122  noetalem1  28128  cutbdaybnd  28211  ltslpss  28324  leslss  28325  coinitslts  28335  addsass  28421  addsdi  28571  mulsass  28582  norecdiv  28606  bdayfinbndlem1  28883  z12bdaylem  28900  brbtwn2  29513  colinearalglem1  29514  colinearalg  29518  axcgrtr  29523  axsegconlem8  29532  axsegconlem9  29533  axsegconlem10  29534  axcontlem8  29579  axcontlem10  29581  elntg2  29593  vtxdlfuhgr1v  30090  umgr2wlk  30568  erclwwlksym  30642  clwwlkfo  30671  clwwlkext2edg  30677  erclwwlknsym  30691  clwwlknon1  30718  numclwwlk2lem1  31007  numclwwlk5  31019  frgrregord13  31027  nvmul0or  31282  ipval2lem2  31336  lnomul  31392  shless  31991  shlej1  31992  pjspansn  32209  hoadddi  32435  kbmul  32587  homco2  32609  kbass2  32749  eliccelico  33439  elicoelioo  33440  iocinioc2  33441  iocinif  33443  swrdrn2  33587  xrge0adddir  33649  xrge0npcan  33651  archiabl  33829  ress1r  33863  grplsm0l  34024  intlidl  34040  ssmxidl  34069  pstmfval  34598  fmcncfil  34633  zrhnm  34669  qqhnm  34692  measvunilem  34915  volfiniune  34933  dya2iocnrect  34983  sibfinima  35041  probun  35121  probinc  35123  cndprob01  35137  signstfvp  35270  bnj517  35585  bnj594  35612  pconnpi1  36169  cvmsss2  36206  mrsubcv  36442  msubvrs  36492  br6  36700  br4  36701  cgrcomim  36932  cgrtriv  36945  cgrextend  36951  segconeq  36953  btwntriv2  36955  btwnintr  36962  btwnexch3  36963  btwnouttr2  36965  trisegint  36971  cgrsub  36988  cgrxfr  36998  btwnxfr  36999  lineext  37019  btwnconn1lem13  37042  btwnconn1lem14  37043  btwnconn3  37046  segcon2  37048  brsegle  37051  brsegle2  37052  segletr  37057  segleantisym  37058  seglelin  37059  outsideofeu  37074  lineunray  37090  lineelsb2  37091  nmulss1  37141  ltnmul  37143  nmulle  37144  ltnadd  37145  naddle  37146  nadddi  37151  ivthALT  37301  weiunpo  37431  weiunso  37432  weiunfr  37433  weiunse  37434  areacirc  38823  cocanfo  38845  upixp  38855  ismtyima  38929  rrndstprj2  38957  zerdivemp1x  39073  lsatfixedN  40258  lssat  40265  eqlkr  40348  eqlkr2  40349  lkrlsp  40351  lshpkrlem4  40362  opposet  40430  cvrcon3b  40526  cvrcmp  40532  atlen0  40559  atnle  40566  atlatmstc  40568  cvlatexch3  40587  cvlsupr2  40592  hlsupr2  40636  hlrelat2  40652  cvrexchlem  40668  lnnat  40676  atcvrj2b  40681  atle  40685  atexchcvrN  40689  atbtwn  40695  athgt  40705  3dimlem3  40710  3dim1  40716  1cvratlt  40723  1cvrjat  40724  ps-1  40726  ps-2  40727  3atlem3  40734  3atlem5  40736  3atlem7  40738  llni  40757  llni2  40761  atcvrlln2  40768  llnexatN  40770  llncmp  40771  2llnmat  40773  2at0mat0  40774  lplni  40781  lplnnle2at  40790  2atnelpln  40793  lplnllnneN  40805  llncvrlpln2  40806  2lplnmN  40808  2llnmj  40809  lplncmp  40811  lplnexatN  40812  lplnexllnN  40813  2llnm3N  40818  lvoli  40824  lvoli3  40826  islvol2aN  40841  4atlem0a  40842  4atlem3  40845  4atlem3a  40846  4atlem4a  40848  4atlem4b  40849  4atlem4c  40850  4atlem4d  40851  4atlem10b  40854  4atlem11  40858  4atlem12  40861  lplncvrlvol2  40864  lvolcmp  40866  2lplnmj  40871  islinei  40989  pmapglbx  41018  linepmap  41024  lneq2at  41027  lnjatN  41029  lncvrat  41031  lncmp  41032  2llnma3r  41037  elpaddatriN  41052  elpaddat  41053  paddcom  41062  paddss1  41066  paddss2  41067  paddss12  41068  paddasslem6  41074  paddasslem7  41075  paddasslem8  41076  paddasslem9  41077  paddasslem15  41083  pmodlem2  41096  pmodl42N  41100  pmapjoin  41101  llnmod1i2  41109  2polcon4bN  41167  polcon2bN  41169  poml4N  41202  poml6N  41204  osumcllem1N  41205  osumcllem2N  41206  osumcllem11N  41215  osumclN  41216  pmapojoinN  41217  pexmidlem2N  41220  pexmidlem3N  41221  pexmidlem4N  41222  pexmidlem6N  41224  pexmidlem7N  41225  pl42lem2N  41229  pl42lem3N  41230  pl42lem4N  41231  pl42N  41232  lhpexle2lem  41258  lhpexle3lem  41260  lhpexle3  41261  lhpmcvr3  41274  lhp2at0nle  41284  lhprelat3N  41289  4atex  41325  4atex2  41326  lauteq  41344  lautco  41346  ltrncoidN  41377  ltrneq2  41397  ltrnnidn  41423  ltrnideq  41424  trlnid  41428  ltrnatlw  41432  trlnle  41435  trlval3  41436  trlval4  41437  cdlemc  41446  cdlemd5  41451  cdlemd9  41455  ltrneq3  41457  cdleme0moN  41474  cdleme20  41573  cdleme21j  41585  cdleme21  41586  cdleme27cl  41615  cdlemefrs29bpre0  41645  cdlemefs27cl  41662  cdlemefs32sn1aw  41663  cdleme43fsv1snlem  41669  cdleme32d  41693  cdleme32f  41695  cdleme32le  41696  cdleme35h2  41706  cdleme38n  41713  cdleme40m  41716  cdleme41snaw  41725  cdleme42ke  41734  cdleme17d3  41745  cdleme48fvg  41749  cdlemeg46fvcl  41755  cdlemeg46fgN  41783  cdleme48gfv1  41785  cdleme48fgv  41787  cdleme50trn3  41802  trlord  41818  ltrniotavalbN  41833  cdlemb3  41855  cdlemg6c  41869  cdlemg6  41872  cdlemg7N  41875  cdlemg8c  41878  cdlemg8  41880  cdlemg11a  41886  cdlemg11b  41891  cdlemg12e  41896  cdlemg15a  41904  cdlemg15  41905  cdlemg16  41906  cdlemg16z  41908  cdlemg16zz  41909  cdlemg17dN  41912  cdlemg18a  41927  cdlemg20  41934  cdlemg22  41936  cdlemg24  41937  cdlemg37  41938  cdlemg31d  41949  cdlemg29  41954  cdlemg33b  41956  cdlemg33  41960  cdlemg38  41964  cdlemg39  41965  cdlemg40  41966  trlco  41976  trlcone  41977  cdlemg42  41978  cdlemg44b  41981  ltrncom  41987  trljco  41989  tendococl  42021  tendoplcl  42030  tendoplcom  42031  cdlemj2  42071  cdlemj3  42072  tendoid0  42074  tendoconid  42078  tendotr  42079  cdlemk25-3  42153  cdlemk26b-3  42154  cdlemk34  42159  cdlemk36  42162  cdlemk38  42164  cdlemkid4  42183  cdlemk35s-id  42187  cdlemk39s-id  42189  cdlemk19x  42192  cdlemk53  42206  cdlemk55  42210  cdlemk55u  42215  cdlemk39u  42217  cdlemk19u  42219  cdlemk56  42220  tendoex  42224  cdleml3N  42227  cdleml5N  42229  tendospcanN  42272  cdlemm10N  42367  cdlemn11pre  42459  dihord2pre  42474  dihvalcqpre  42484  dihopelvalcpre  42497  dihord6apre  42505  dihord5b  42508  dihord5apre  42511  dihord  42513  dihmeetlem1N  42539  dihglblem5apreN  42540  dihglblem3N  42544  dihmeetlem2N  42548  dihglbcpreN  42549  dihmeetbN  42552  dihmeetlem4preN  42555  dihmeetlem5  42557  dihmeetlem7N  42559  dihmeetlem10N  42565  dihmeetlem11N  42566  dihmeetlem12N  42567  dihmeetlem13N  42568  dihmeetlem15N  42570  dihmeetlem16N  42571  dihmeetlem17N  42572  dihmeetlem18N  42573  dihmeetlem19N  42574  dihmeetALTN  42576  dih1dimatlem0  42577  dihlspsnssN  42581  dihlspsnat  42582  mapdh8ad  43028  hdmap14lem14  43130  hgmapvvlem3  43174  aks6d1c6isolem1  43416  resubcan2  43632  mzprename  43953  eldioph2lem1  43964  lzunuz  43972  rencldnfi  44021  pellexlem2  44030  infmrgelbi  44078  pellfundglb  44085  pellfund14gap  44087  qirropth  44108  rmxycomplete  44117  congadd  44166  acongeq  44183  jm2.19  44193  jm2.23  44196  jm2.20nn  44197  jm2.27  44208  jm3.1  44220  aomclem6  44254  lnmepi  44280  lmhmfgsplit  44281  lmhmlnmsplit  44282  pwssplit4  44284  hbtlem2  44318  hbtlem5  44322  dgraa0p  44343  proot1hash  44389  iocunico  44405  oasubex  44480  oege1  44500  relexpxpmin  44909  brtrclfv2  44919  ntrclsiso  45259  ntrclskb  45261  ntrclsk3  45262  k0004lem3  45341  grur1cld  45422  ismnu  45437  grumnudlem  45461  suprnmpt  46394  wessf1ornlem  46405  projf1o  46416  snunioo1  46729  iccintsng  46740  lptre2pt  46855  limcleqr  46859  fnlimfvre  46889  limsupgtlem  46992  volioc  47187  iblspltprt  47188  stoweidlem19  47234  stoweidlem20  47235  stoweidlem22  47237  stoweidlem28  47243  stoweidlem34  47249  stoweidlem44  47259  stoweidlem60  47275  wallispilem3  47282  fourierdlem41  47363  fourierdlem42  47364  fourierdlem49  47370  fourierdlem51  47372  fourierdlem54  47375  fourierdlem74  47395  fourierdlem97  47418  caratheodorylem2  47742  ovnsubaddlem2  47786  hspmbllem2  47842  smflimmpt  48025  smflimsupmpt  48044  smfliminfmpt  48047  funfocofob  48353  fzopredsuc  48599  nnmul2b  48606  imasetpreimafvbijlemfv  48689  iccpartigtl  48710  lighneal  48901  oexpnegALTV  48980  oexpnegnz  48981  tgblthelfgott  49118  clnbgrgrim  49237  uhgrimgrlim  49290  gpgusgralem  49359  lidldomn1  49533  ofaddmndmap  49660  lincdifsn  49741  lincellss  49743  lincresunit3lem3  49791  islindeps2  49800  lindssnlvec  49803  fdivmptf  49858  refdivmptf  49859  rrx2linest  50059  itsclc0yqsollem1  50079  itsclc0b  50089  itsclquadb  50093  itscnhlinecirc02plem3  50101  diag1  50631  setc1onsubc  50945