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  1501  rspc3ev  3592  2nreu  4401  predtrss  6325  frpomin  6343  f1prex  7292  cocan1  7299  weniso  7364  frrlem4  8310  frrlem10  8316  fprlem1  8321  smogt  8378  smocdmdom  8379  omeulem1  8593  nnmord  8644  nnmword  8645  naddasslem1  8707  naddasslem2  8708  difsnen  9081  enfixsn  9108  mapunen  9168  ac6sfi  9278  fissorduni  9285  fipreima  9350  elfiun  9425  ordiso2  9512  wemaplem2  9544  en2eqpr  10089  indcardi  10123  fodomfi2  10142  iunfictbso  10196  infmap2  10298  cofsmo  10350  cfsmolem  10351  coftr  10354  fin23lem11  10398  fincssdom  10404  fin23lem26  10406  isf32lem9  10442  ac6num  10560  gchdomtri  10717  gchpwdom  10758  winainflem  10781  tskuni  10871  gruima  10890  gruf  10899  grudomon  10905  elnpi  11076  distrlem4pr  11114  prlem934  11121  addcan  11497  addcan2  11498  divmulass  12000  divmulasscom  12001  ltmul1a  12169  suprleub  12286  supmul1  12289  suprzcl  12782  uzsupss  13070  xleadd1a  13386  xlesubadd  13396  xmulasslem3  13419  xlemul2a  13422  xadddilem  13427  xadddi2  13430  ixxun  13495  icoshftf1o  13608  ioounsn  13611  snunioc  13614  lincmb01cmp  13629  iccf1o  13630  nn0p1elfzo  13840  fzofzim  13847  fzoopth  13900  ltexp2a  14312  leexp2  14317  ltexp2r  14319  exple1  14323  expnlbnd2  14381  fun2dmnop0  14652  ccatass  14737  swrdswrdlem  14857  ccatopth  14869  repswpfx  14940  2cshw  14968  cshimadifsn  14984  cshimadifsn0  14985  cshco  14991  repsco  14995  s2f1o  15072  limsupgre  15653  addcn2  15766  mulcn2  15768  ntrivcvgmul  16076  binomrisefac  16213  dvdsmodexp  16435  dvdsadd2b  16481  dvdsexp2im  16502  dvdsmod  16504  oexpneg  16520  sadass  16646  gcdass  16725  rplpwr  16737  dvdsexpnn  16745  lcmfunsnlem1  16817  coprmdvds2  16834  rpmulgcd2  16836  qredeq  16837  rpdvds  16840  cncongr2  16848  rpexp  16903  prmdiveq  16968  hashgcdlem  16970  odzdvds  16978  modprmn0modprm0  16990  coprimeprodsq2  16992  pythagtriplem3  17001  pcdvdsb  17052  pcgcd1  17060  qexpz  17084  pockthg  17089  vdwnnlem1  17178  0ram  17203  ramz2  17207  lubss  18692  lubun  18694  clatleglb  18697  clatglbss  18698  mrelatglb  18739  isnsgrp  18917  issubmnd  18958  ress0gOLD  18960  mhmvlin  19001  gsumccat  19042  frmdss2  19064  submefmnd  19096  mulgneg  19307  mulgdirlem  19320  submmulg  19333  subgmulg  19356  nmzsubg  19380  ghmmulg  19447  gsmsymgreqlem1  19649  pmtrfb  19684  psgnunilem4  19716  odmodnn0  19759  odnncl  19764  odmod  19765  odmulgid  19773  odmulgeq  19776  odf1o1  19791  odf1o2  19792  odngen  19796  gexdvdsi  19802  pgpfi1  19814  odcau  19823  subgslw  19835  fislw  19844  lsmssv  19862  lsmless1x  19863  lsmless2x  19864  lsmsubm  19872  lsmmod  19894  lsmmod2  19895  efgred  19967  cntzcmn  20059  ghmplusg  20065  odadd1  20067  odadd2  20068  odadd  20069  lsmcomx  20075  gsumconst  20153  ablsimpgprmd  20336  ring1eq0  20534  mulgass2  20545  rngisom1  20701  rhmdvdsr  20763  isabvd  21074  rmodislmodlem  21209  rmodislmod  21210  lssintcl  21244  0lmhm  21320  lmhmvsca  21325  reslmhm2b  21334  pwssplit1  21339  pwssplit3  21341  lspfixed  21411  lspsnat  21428  unichnlidl  21521  pidlnz  21533  rnglidlrng  21540  2idlcpblrng  21570  lidldvgen  21663  xrsdsreclblem  21724  regsumsupp  21933  obselocv  22039  uvcresum  22104  frlmsslsp  22107  frlmup4  22112  lindff1  22131  f1lindf  22133  lsslindf  22141  islindf4  22149  lbslcic  22152  lindsenlbs  22162  issubassa  22180  evlsval2  22401  psrplusgpropd  22558  coe1subfv  22590  coe1mul2  22593  mpomatmul  22766  mamutpos  22778  scmatscmide  22827  mavmulsolcl  22871  marrepcl  22884  mdetdiag  22919  mdetunilem1  22932  mdetunilem3  22934  mdetunilem7  22938  mdetunilem9  22940  mdetmul  22943  slesolinvbi  23004  m2pmfzmap  23070  pmatcollpwlem  23103  pmatcollpw  23104  mp2pm2mplem4  23132  chpdmatlem3  23163  chfacfisfcpmat  23178  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  chfacfpmmulgsum2  23188  cayhamlem1  23189  cpmidpmatlem2  23194  cpmadugsumlemB  23197  cpmadugsumlemC  23198  cpmadugsumlemF  23199  riinopn  23231  neiint  23427  topssnei  23447  restntr  23505  iscnp4  23586  cnconst2  23606  cnrest2  23609  cnprest2  23613  cnpdis  23616  cnt0  23669  cnt1  23673  cnhaus  23677  ordthauslem  23706  cncmp  23715  fiuncmp  23727  sscmp  23728  hauscmp  23730  cnconn  23745  unconn  23752  nlly2i  23800  llynlly  23801  nllyidm  23813  finlocfin  23844  ptrescn  23963  xkococnlem  23983  qtopss  24039  kqfvima  24054  r0cld  24062  ordthmeolem  24125  fbssint  24162  fmf  24269  fmss  24270  elfm  24271  rnelfmlem  24276  rnelfm  24277  fmco  24285  flimss2  24296  flimss1  24297  flimrest  24307  flftg  24320  cnpflf2  24324  cnpflf  24325  flfcnp  24328  supnfcls  24344  fclsss1  24346  fclsss2  24347  fcfnei  24359  fcfelbas  24360  cnpfcfi  24364  subgntr  24431  opnsubg  24432  cldsubg  24435  ghmcnp  24439  utop2nei  24574  neipcfilu  24619  bldisj  24722  blgt0  24723  bl2in  24724  blss2ps  24727  blss2  24728  blssps  24748  blss  24749  xmetresbl  24761  lpbl  24827  blcld  24829  stdbdbl  24841  metcnp3  24864  metcnp2  24866  txmetcnp  24871  blval2  24886  nmoix  25053  nmoeq0  25060  icoopnst  25265  iocopnst  25266  xrhmeo  25272  nmhmcn  25446  cphsqrtcl2  25512  cphsqrtcl3  25513  cfil3i  25595  caublcls  25635  bcthlem5  25654  cmetcusp1  25679  cssbn  25701  rrxcph  25718  pjth  25765  ovoliunlem2  25829  volun  25871  volsup2  25931  mbfimaopn2  25983  iblconst  26143  itgconst  26144  dvcnp2  26245  dvcn  26246  deg1mul3le  26440  deg1tmle  26441  dvdsq1p  26486  ig1peu  26498  ig1pdvds  26503  coeid3  26564  dgrmulc  26595  efcvx  26781  tanord  26871  logdivlti  26953  logccv  26996  recxpcl  27008  cxpeq  27090  ang180  27147  isosctrlem2  27152  cxp2lim  27309  amgm  27323  muval1  27465  dvdssqf  27470  mumullem2  27512  mumul  27513  bcmono  27609  lgsfcl2  27635  lgsdilem  27656  lgsdirprm  27663  lgsdir  27664  lgsdi  27666  lgsne0  27667  padicabv  27962  nosep1o  28043  nosep2o  28044  nosepssdm  28048  nolt02olem  28056  nosupres  28069  nosupbnd1lem1  28070  nosupbnd1lem4  28073  nosupbnd1lem5  28074  nosupbnd1lem6  28075  nosupbnd2  28078  noinfres  28084  noinfbnd1lem1  28085  noinfbnd1lem4  28088  noinfbnd1lem6  28090  noinfbnd2  28093  noetasuplem3  28097  noetalem1  28103  cutbdaybnd  28186  ltslpss  28299  leslss  28300  coinitslts  28310  addsass  28396  addsdi  28546  mulsass  28557  norecdiv  28581  bdayfinbndlem1  28858  z12bdaylem  28875  brbtwn2  29488  colinearalglem1  29489  colinearalg  29493  axcgrtr  29498  axsegconlem8  29507  axsegconlem9  29508  axsegconlem10  29509  axcontlem8  29554  axcontlem10  29556  elntg2  29568  vtxdlfuhgr1v  30065  umgr2wlk  30543  erclwwlksym  30617  clwwlkfo  30646  clwwlkext2edg  30652  erclwwlknsym  30666  clwwlknon1  30693  numclwwlk2lem1  30982  numclwwlk5  30994  frgrregord13  31002  nvmul0or  31257  ipval2lem2  31311  lnomul  31367  shless  31966  shlej1  31967  pjspansn  32184  hoadddi  32410  kbmul  32562  homco2  32584  kbass2  32724  eliccelico  33415  elicoelioo  33416  iocinioc2  33417  iocinif  33419  swrdrn2  33563  xrge0adddir  33625  xrge0npcan  33627  archiabl  33805  ress1r  33839  grplsm0l  34000  intlidl  34016  ssmxidl  34045  pstmfval  34574  fmcncfil  34609  zrhnm  34645  qqhnm  34668  measvunilem  34891  volfiniune  34909  dya2iocnrect  34959  sibfinima  35017  probun  35097  probinc  35099  cndprob01  35113  signstfvp  35246  bnj517  35561  bnj594  35588  pconnpi1  36088  cvmsss2  36125  mrsubcv  36361  msubvrs  36411  br6  36614  br4  36615  cgrcomim  36846  cgrtriv  36859  cgrextend  36865  segconeq  36867  btwntriv2  36869  btwnintr  36876  btwnexch3  36877  btwnouttr2  36879  trisegint  36885  cgrsub  36902  cgrxfr  36912  btwnxfr  36913  lineext  36933  btwnconn1lem13  36956  btwnconn1lem14  36957  btwnconn3  36960  segcon2  36962  brsegle  36965  brsegle2  36966  segletr  36971  segleantisym  36972  seglelin  36973  outsideofeu  36988  lineunray  37004  lineelsb2  37005  nmulss1  37055  ltnmul  37057  nmulle  37058  ltnadd  37059  naddle  37060  nadddi  37065  ivthALT  37215  weiunpo  37345  weiunso  37346  weiunfr  37347  weiunse  37348  areacirc  38724  cocanfo  38746  upixp  38756  ismtyima  38830  rrndstprj2  38858  zerdivemp1x  38974  lsatfixedN  40159  lssat  40166  eqlkr  40249  eqlkr2  40250  lkrlsp  40252  lshpkrlem4  40263  opposet  40331  cvrcon3b  40427  cvrcmp  40433  atlen0  40460  atnle  40467  atlatmstc  40469  cvlatexch3  40488  cvlsupr2  40493  hlsupr2  40537  hlrelat2  40553  cvrexchlem  40569  lnnat  40577  atcvrj2b  40582  atle  40586  atexchcvrN  40590  atbtwn  40596  athgt  40606  3dimlem3  40611  3dim1  40617  1cvratlt  40624  1cvrjat  40625  ps-1  40627  ps-2  40628  3atlem3  40635  3atlem5  40637  3atlem7  40639  llni  40658  llni2  40662  atcvrlln2  40669  llnexatN  40671  llncmp  40672  2llnmat  40674  2at0mat0  40675  lplni  40682  lplnnle2at  40691  2atnelpln  40694  lplnllnneN  40706  llncvrlpln2  40707  2lplnmN  40709  2llnmj  40710  lplncmp  40712  lplnexatN  40713  lplnexllnN  40714  2llnm3N  40719  lvoli  40725  lvoli3  40727  islvol2aN  40742  4atlem0a  40743  4atlem3  40746  4atlem3a  40747  4atlem4a  40749  4atlem4b  40750  4atlem4c  40751  4atlem4d  40752  4atlem10b  40755  4atlem11  40759  4atlem12  40762  lplncvrlvol2  40765  lvolcmp  40767  2lplnmj  40772  islinei  40890  pmapglbx  40919  linepmap  40925  lneq2at  40928  lnjatN  40930  lncvrat  40932  lncmp  40933  2llnma3r  40938  elpaddatriN  40953  elpaddat  40954  paddcom  40963  paddss1  40967  paddss2  40968  paddss12  40969  paddasslem6  40975  paddasslem7  40976  paddasslem8  40977  paddasslem9  40978  paddasslem15  40984  pmodlem2  40997  pmodl42N  41001  pmapjoin  41002  llnmod1i2  41010  2polcon4bN  41068  polcon2bN  41070  poml4N  41103  poml6N  41105  osumcllem1N  41106  osumcllem2N  41107  osumcllem11N  41116  osumclN  41117  pmapojoinN  41118  pexmidlem2N  41121  pexmidlem3N  41122  pexmidlem4N  41123  pexmidlem6N  41125  pexmidlem7N  41126  pl42lem2N  41130  pl42lem3N  41131  pl42lem4N  41132  pl42N  41133  lhpexle2lem  41159  lhpexle3lem  41161  lhpexle3  41162  lhpmcvr3  41175  lhp2at0nle  41185  lhprelat3N  41190  4atex  41226  4atex2  41227  lauteq  41245  lautco  41247  ltrncoidN  41278  ltrneq2  41298  ltrnnidn  41324  ltrnideq  41325  trlnid  41329  ltrnatlw  41333  trlnle  41336  trlval3  41337  trlval4  41338  cdlemc  41347  cdlemd5  41352  cdlemd9  41356  ltrneq3  41358  cdleme0moN  41375  cdleme20  41474  cdleme21j  41486  cdleme21  41487  cdleme27cl  41516  cdlemefrs29bpre0  41546  cdlemefs27cl  41563  cdlemefs32sn1aw  41564  cdleme43fsv1snlem  41570  cdleme32d  41594  cdleme32f  41596  cdleme32le  41597  cdleme35h2  41607  cdleme38n  41614  cdleme40m  41617  cdleme41snaw  41626  cdleme42ke  41635  cdleme17d3  41646  cdleme48fvg  41650  cdlemeg46fvcl  41656  cdlemeg46fgN  41684  cdleme48gfv1  41686  cdleme48fgv  41688  cdleme50trn3  41703  trlord  41719  ltrniotavalbN  41734  cdlemb3  41756  cdlemg6c  41770  cdlemg6  41773  cdlemg7N  41776  cdlemg8c  41779  cdlemg8  41781  cdlemg11a  41787  cdlemg11b  41792  cdlemg12e  41797  cdlemg15a  41805  cdlemg15  41806  cdlemg16  41807  cdlemg16z  41809  cdlemg16zz  41810  cdlemg17dN  41813  cdlemg18a  41828  cdlemg20  41835  cdlemg22  41837  cdlemg24  41838  cdlemg37  41839  cdlemg31d  41850  cdlemg29  41855  cdlemg33b  41857  cdlemg33  41861  cdlemg38  41865  cdlemg39  41866  cdlemg40  41867  trlco  41877  trlcone  41878  cdlemg42  41879  cdlemg44b  41882  ltrncom  41888  trljco  41890  tendococl  41922  tendoplcl  41931  tendoplcom  41932  cdlemj2  41972  cdlemj3  41973  tendoid0  41975  tendoconid  41979  tendotr  41980  cdlemk25-3  42054  cdlemk26b-3  42055  cdlemk34  42060  cdlemk36  42063  cdlemk38  42065  cdlemkid4  42084  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk19x  42093  cdlemk53  42107  cdlemk55  42111  cdlemk55u  42116  cdlemk39u  42118  cdlemk19u  42120  cdlemk56  42121  tendoex  42125  cdleml3N  42128  cdleml5N  42130  tendospcanN  42173  cdlemm10N  42268  cdlemn11pre  42360  dihord2pre  42375  dihvalcqpre  42385  dihopelvalcpre  42398  dihord6apre  42406  dihord5b  42409  dihord5apre  42412  dihord  42414  dihmeetlem1N  42440  dihglblem5apreN  42441  dihglblem3N  42445  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetbN  42453  dihmeetlem4preN  42456  dihmeetlem5  42458  dihmeetlem7N  42460  dihmeetlem10N  42466  dihmeetlem11N  42467  dihmeetlem12N  42468  dihmeetlem13N  42469  dihmeetlem15N  42471  dihmeetlem16N  42472  dihmeetlem17N  42473  dihmeetlem18N  42474  dihmeetlem19N  42475  dihmeetALTN  42477  dih1dimatlem0  42478  dihlspsnssN  42482  dihlspsnat  42483  mapdh8ad  42929  hdmap14lem14  43031  hgmapvvlem3  43075  aks6d1c6isolem1  43317  resubcan2  43532  mzprename  43853  eldioph2lem1  43864  lzunuz  43872  rencldnfi  43921  pellexlem2  43930  infmrgelbi  43978  pellfundglb  43985  pellfund14gap  43987  qirropth  44008  rmxycomplete  44017  congadd  44066  acongeq  44083  jm2.19  44093  jm2.23  44096  jm2.20nn  44097  jm2.27  44108  jm3.1  44120  aomclem6  44154  lnmepi  44180  lmhmfgsplit  44181  lmhmlnmsplit  44182  pwssplit4  44184  hbtlem2  44219  hbtlem5  44223  dgraa0p  44244  proot1hash  44290  iocunico  44306  oasubex  44381  oege1  44401  relexpxpmin  44810  brtrclfv2  44820  ntrclsiso  45160  ntrclskb  45162  ntrclsk3  45163  k0004lem3  45242  grur1cld  45323  ismnu  45338  grumnudlem  45362  suprnmpt  46282  wessf1ornlem  46293  projf1o  46304  snunioo1  46617  iccintsng  46628  lptre2pt  46743  limcleqr  46747  fnlimfvre  46777  limsupgtlem  46880  volioc  47075  iblspltprt  47076  stoweidlem19  47122  stoweidlem20  47123  stoweidlem22  47125  stoweidlem28  47131  stoweidlem34  47137  stoweidlem44  47147  stoweidlem60  47163  wallispilem3  47170  fourierdlem41  47251  fourierdlem42  47252  fourierdlem49  47258  fourierdlem51  47260  fourierdlem54  47263  fourierdlem74  47283  fourierdlem97  47306  caratheodorylem2  47630  ovnsubaddlem2  47674  hspmbllem2  47730  smflimmpt  47913  smflimsupmpt  47932  smfliminfmpt  47935  funfocofob  48241  fzopredsuc  48487  nnmul2b  48494  imasetpreimafvbijlemfv  48577  iccpartigtl  48598  lighneal  48789  oexpnegALTV  48868  oexpnegnz  48869  tgblthelfgott  49006  clnbgrgrim  49125  uhgrimgrlim  49178  gpgusgralem  49247  lidldomn1  49421  ofaddmndmap  49548  lincdifsn  49629  lincellss  49631  lincresunit3lem3  49679  islindeps2  49688  lindssnlvec  49691  fdivmptf  49746  refdivmptf  49747  rrx2linest  49947  itsclc0yqsollem1  49967  itsclc0b  49977  itsclquadb  49981  itscnhlinecirc02plem3  49989  diag1  50519  setc1onsubc  50833