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  3601  2nreu  4412  predtrss  6330  frpomin  6348  f1prex  7293  cocan1  7300  weniso  7365  frrlem4  8295  frrlem10  8301  fprlem1  8306  smogt  8363  smocdmdom  8364  omeulem1  8576  nnmord  8627  nnmword  8628  naddasslem1  8690  naddasslem2  8691  difsnen  9057  enfixsn  9084  mapunen  9144  ac6sfi  9254  fipreima  9325  elfiun  9400  ordiso2  9487  wemaplem2  9519  en2eqpr  10010  indcardi  10044  fodomfi2  10063  iunfictbso  10117  infmap2  10219  cofsmo  10271  cfsmolem  10272  coftr  10275  fin23lem11  10319  fincssdom  10325  fin23lem26  10327  isf32lem9  10363  ac6num  10481  gchdomtri  10632  gchpwdom  10673  winainflem  10696  tskuni  10786  gruima  10805  gruf  10814  grudomon  10820  elnpi  10991  distrlem4pr  11029  prlem934  11036  addcan  11412  addcan2  11413  divmulass  11913  divmulasscom  11914  ltmul1a  12082  suprleub  12199  supmul1  12202  suprzcl  12694  uzsupss  12982  xleadd1a  13297  xlesubadd  13307  xmulasslem3  13330  xlemul2a  13333  xadddilem  13338  xadddi2  13341  ixxun  13406  icoshftf1o  13519  ioounsn  13522  snunioc  13525  lincmb01cmp  13540  iccf1o  13541  nn0p1elfzo  13750  fzofzim  13757  fzoopth  13810  ltexp2a  14222  leexp2  14227  ltexp2r  14229  exple1  14233  expnlbnd2  14290  fun2dmnop0  14561  ccatass  14646  swrdswrdlem  14765  ccatopth  14777  repswpfx  14848  2cshw  14876  cshimadifsn  14892  cshimadifsn0  14893  cshco  14899  repsco  14903  s2f1o  14979  limsupgre  15558  addcn2  15671  mulcn2  15673  ntrivcvgmul  15982  binomrisefac  16121  dvdsmodexp  16343  dvdsadd2b  16389  dvdsexp2im  16410  dvdsmod  16412  oexpneg  16428  sadass  16554  gcdass  16630  rplpwr  16641  lcmfunsnlem1  16720  coprmdvds2  16737  rpmulgcd2  16739  qredeq  16740  rpdvds  16743  cncongr2  16751  rpexp  16806  prmdiveq  16870  hashgcdlem  16872  odzdvds  16880  modprmn0modprm0  16892  coprimeprodsq2  16894  pythagtriplem3  16903  pcdvdsb  16954  pcgcd1  16962  qexpz  16986  pockthg  16991  vdwnnlem1  17080  0ram  17105  ramz2  17109  lubss  18594  lubun  18596  clatleglb  18599  clatglbss  18600  mrelatglb  18641  isnsgrp  18810  issubmnd  18848  ress0gOLD  18850  mhmvlin  18890  gsumccat  18931  frmdss2  18953  submefmnd  18985  mulgneg  19189  mulgdirlem  19202  submmulg  19215  subgmulg  19238  nmzsubg  19262  ghmmulg  19329  gsmsymgreqlem1  19531  pmtrfb  19566  psgnunilem4  19598  odmodnn0  19641  odnncl  19646  odmod  19647  odmulgid  19655  odmulgeq  19658  odf1o1  19673  odf1o2  19674  odngen  19678  gexdvdsi  19684  pgpfi1  19696  odcau  19705  subgslw  19717  fislw  19726  lsmssv  19744  lsmless1x  19745  lsmless2x  19746  lsmsubm  19754  lsmmod  19776  lsmmod2  19777  efgred  19849  cntzcmn  19941  ghmplusg  19947  odadd1  19949  odadd2  19950  odadd  19951  lsmcomx  19957  gsumconst  20035  ablsimpgprmd  20218  ring1eq0  20414  mulgass2  20425  rngisom1  20581  rhmdvdsr  20642  isabvd  20952  rmodislmodlem  21087  rmodislmod  21088  lssintcl  21122  0lmhm  21198  lmhmvsca  21203  reslmhm2b  21212  pwssplit1  21217  pwssplit3  21219  lspfixed  21289  lspsnat  21306  unichnlidl  21399  pidlnz  21411  rnglidlrng  21418  2idlcpblrng  21447  lidldvgen  21539  xrsdsreclblem  21600  regsumsupp  21809  obselocv  21915  uvcresum  21980  frlmsslsp  21983  frlmup4  21988  lindff1  22007  f1lindf  22009  lsslindf  22017  islindf4  22025  lbslcic  22028  issubassa  22054  evlsval2  22275  psrplusgpropd  22432  coe1subfv  22464  coe1mul2  22467  mpomatmul  22640  mamutpos  22652  scmatscmide  22701  mavmulsolcl  22745  marrepcl  22758  mdetdiag  22793  mdetunilem1  22806  mdetunilem3  22808  mdetunilem7  22812  mdetunilem9  22814  mdetmul  22817  slesolinvbi  22875  m2pmfzmap  22941  pmatcollpwlem  22974  pmatcollpw  22975  mp2pm2mplem4  23003  chpdmatlem3  23034  chfacfisfcpmat  23049  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  chfacfpmmulgsum2  23059  cayhamlem1  23060  cpmidpmatlem2  23065  cpmadugsumlemB  23068  cpmadugsumlemC  23069  cpmadugsumlemF  23070  riinopn  23102  neiint  23298  topssnei  23318  restntr  23376  iscnp4  23457  cnconst2  23477  cnrest2  23480  cnprest2  23484  cnpdis  23487  cnt0  23540  cnt1  23544  cnhaus  23548  ordthauslem  23577  cncmp  23586  fiuncmp  23598  sscmp  23599  hauscmp  23601  cnconn  23616  unconn  23623  nlly2i  23670  llynlly  23671  nllyidm  23683  finlocfin  23714  ptrescn  23833  xkococnlem  23853  qtopss  23909  kqfvima  23924  r0cld  23932  ordthmeolem  23995  fbssint  24032  fmf  24139  fmss  24140  elfm  24141  rnelfmlem  24146  rnelfm  24147  fmco  24155  flimss2  24166  flimss1  24167  flimrest  24177  flftg  24190  cnpflf2  24194  cnpflf  24195  flfcnp  24198  supnfcls  24214  fclsss1  24216  fclsss2  24217  fcfnei  24229  fcfelbas  24230  cnpfcfi  24234  subgntr  24301  opnsubg  24302  cldsubg  24305  ghmcnp  24309  utop2nei  24444  neipcfilu  24489  bldisj  24592  blgt0  24593  bl2in  24594  blss2ps  24597  blss2  24598  blssps  24618  blss  24619  xmetresbl  24631  lpbl  24697  blcld  24699  stdbdbl  24711  metcnp3  24734  metcnp2  24736  txmetcnp  24741  blval2  24756  nmoix  24923  nmoeq0  24930  icoopnst  25135  iocopnst  25136  xrhmeo  25142  nmhmcn  25316  cphsqrtcl2  25382  cphsqrtcl3  25383  cfil3i  25465  caublcls  25505  bcthlem5  25524  cmetcusp1  25549  cssbn  25571  rrxcph  25588  pjth  25635  ovoliunlem2  25699  volun  25741  volsup2  25801  mbfimaopn2  25853  iblconst  26014  itgconst  26015  dvcnp2  26116  dvcn  26117  deg1mul3le  26311  deg1tmle  26312  dvdsq1p  26357  ig1peu  26369  ig1pdvds  26374  coeid3  26434  dgrmulc  26465  efcvx  26649  tanord  26740  logdivlti  26822  logccv  26865  recxpcl  26877  cxpeq  26959  ang180  27016  isosctrlem2  27021  cxp2lim  27178  amgm  27192  muval1  27334  dvdssqf  27339  mumullem2  27381  mumul  27382  bcmono  27478  lgsfcl2  27504  lgsdilem  27525  lgsdirprm  27532  lgsdir  27533  lgsdi  27535  lgsne0  27536  padicabv  27831  nosep1o  27882  nosep2o  27883  nosepssdm  27887  nolt02olem  27895  nosupres  27908  nosupbnd1lem1  27909  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd1lem6  27914  nosupbnd2  27917  noinfres  27923  noinfbnd1lem1  27924  noinfbnd1lem4  27927  noinfbnd1lem6  27929  noinfbnd2  27932  noetasuplem3  27936  noetalem1  27942  cutbdaybnd  28025  ltslpss  28138  leslss  28139  coinitslts  28149  addsass  28235  addsdi  28385  mulsass  28396  norecdiv  28420  bdayfinbndlem1  28697  z12bdaylem  28714  brbtwn2  29292  colinearalglem1  29293  colinearalg  29297  axcgrtr  29302  axsegconlem8  29311  axsegconlem9  29312  axsegconlem10  29313  axcontlem8  29358  axcontlem10  29360  elntg2  29372  vtxdlfuhgr1v  29866  umgr2wlk  30335  erclwwlksym  30409  clwwlkfo  30438  clwwlkext2edg  30444  erclwwlknsym  30458  clwwlknon1  30485  numclwwlk2lem1  30764  numclwwlk5  30776  frgrregord13  30784  nvmul0or  31039  ipval2lem2  31093  lnomul  31149  shless  31748  shlej1  31749  pjspansn  31966  hoadddi  32192  kbmul  32344  homco2  32366  kbass2  32506  eliccelico  33159  elicoelioo  33160  iocinioc2  33161  iocinif  33163  swrdrn2  33307  xrge0adddir  33369  xrge0npcan  33371  archiabl  33549  ress1r  33583  grplsm0l  33743  intlidl  33759  ssmxidl  33788  pstmfval  34317  fmcncfil  34352  zrhnm  34388  qqhnm  34411  measvunilem  34634  volfiniune  34652  dya2iocnrect  34703  sibfinima  34761  probun  34841  probinc  34843  cndprob01  34857  signstfvp  34990  bnj517  35305  bnj594  35332  fissorduni  35505  pconnpi1  35750  cvmsss2  35787  mrsubcv  36023  msubvrs  36073  br6  36270  br4  36271  cgrcomim  36502  cgrtriv  36515  cgrextend  36521  segconeq  36523  btwntriv2  36525  btwnintr  36532  btwnexch3  36533  btwnouttr2  36535  trisegint  36541  cgrsub  36558  cgrxfr  36568  btwnxfr  36569  lineext  36589  btwnconn1lem13  36612  btwnconn1lem14  36613  btwnconn3  36616  segcon2  36618  brsegle  36621  brsegle2  36622  segletr  36627  segleantisym  36628  seglelin  36629  outsideofeu  36644  lineunray  36660  lineelsb2  36661  nmulss1  36727  ltnmul  36729  nmulle  36730  ltnadd  36731  naddle  36732  nadddi  36737  ivthALT  36887  weiunpo  37017  weiunso  37018  weiunfr  37019  weiunse  37020  lindsenlbs  38307  areacirc  38405  cocanfo  38411  upixp  38421  ismtyima  38495  rrndstprj2  38523  zerdivemp1x  38639  lsatfixedN  39824  lssat  39831  eqlkr  39914  eqlkr2  39915  lkrlsp  39917  lshpkrlem4  39928  opposet  39996  cvrcon3b  40092  cvrcmp  40098  atlen0  40125  atnle  40132  atlatmstc  40134  cvlatexch3  40153  cvlsupr2  40158  hlsupr2  40202  hlrelat2  40218  cvrexchlem  40234  lnnat  40242  atcvrj2b  40247  atle  40251  atexchcvrN  40255  atbtwn  40261  athgt  40271  3dimlem3  40276  3dim1  40282  1cvratlt  40289  1cvrjat  40290  ps-1  40292  ps-2  40293  3atlem3  40300  3atlem5  40302  3atlem7  40304  llni  40323  llni2  40327  atcvrlln2  40334  llnexatN  40336  llncmp  40337  2llnmat  40339  2at0mat0  40340  lplni  40347  lplnnle2at  40356  2atnelpln  40359  lplnllnneN  40371  llncvrlpln2  40372  2lplnmN  40374  2llnmj  40375  lplncmp  40377  lplnexatN  40378  lplnexllnN  40379  2llnm3N  40384  lvoli  40390  lvoli3  40392  islvol2aN  40407  4atlem0a  40408  4atlem3  40411  4atlem3a  40412  4atlem4a  40414  4atlem4b  40415  4atlem4c  40416  4atlem4d  40417  4atlem10b  40420  4atlem11  40424  4atlem12  40427  lplncvrlvol2  40430  lvolcmp  40432  2lplnmj  40437  islinei  40555  pmapglbx  40584  linepmap  40590  lneq2at  40593  lnjatN  40595  lncvrat  40597  lncmp  40598  2llnma3r  40603  elpaddatriN  40618  elpaddat  40619  paddcom  40628  paddss1  40632  paddss2  40633  paddss12  40634  paddasslem6  40640  paddasslem7  40641  paddasslem8  40642  paddasslem9  40643  paddasslem15  40649  pmodlem2  40662  pmodl42N  40666  pmapjoin  40667  llnmod1i2  40675  2polcon4bN  40733  polcon2bN  40735  poml4N  40768  poml6N  40770  osumcllem1N  40771  osumcllem2N  40772  osumcllem11N  40781  osumclN  40782  pmapojoinN  40783  pexmidlem2N  40786  pexmidlem3N  40787  pexmidlem4N  40788  pexmidlem6N  40790  pexmidlem7N  40791  pl42lem2N  40795  pl42lem3N  40796  pl42lem4N  40797  pl42N  40798  lhpexle2lem  40824  lhpexle3lem  40826  lhpexle3  40827  lhpmcvr3  40840  lhp2at0nle  40850  lhprelat3N  40855  4atex  40891  4atex2  40892  lauteq  40910  lautco  40912  ltrncoidN  40943  ltrneq2  40963  ltrnnidn  40989  ltrnideq  40990  trlnid  40994  ltrnatlw  40998  trlnle  41001  trlval3  41002  trlval4  41003  cdlemc  41012  cdlemd5  41017  cdlemd9  41021  ltrneq3  41023  cdleme0moN  41040  cdleme20  41139  cdleme21j  41151  cdleme21  41152  cdleme27cl  41181  cdlemefrs29bpre0  41211  cdlemefs27cl  41228  cdlemefs32sn1aw  41229  cdleme43fsv1snlem  41235  cdleme32d  41259  cdleme32f  41261  cdleme32le  41262  cdleme35h2  41272  cdleme38n  41279  cdleme40m  41282  cdleme41snaw  41291  cdleme42ke  41300  cdleme17d3  41311  cdleme48fvg  41315  cdlemeg46fvcl  41321  cdlemeg46fgN  41349  cdleme48gfv1  41351  cdleme48fgv  41353  cdleme50trn3  41368  trlord  41384  ltrniotavalbN  41399  cdlemb3  41421  cdlemg6c  41435  cdlemg6  41438  cdlemg7N  41441  cdlemg8c  41444  cdlemg8  41446  cdlemg11a  41452  cdlemg11b  41457  cdlemg12e  41462  cdlemg15a  41470  cdlemg15  41471  cdlemg16  41472  cdlemg16z  41474  cdlemg16zz  41475  cdlemg17dN  41478  cdlemg18a  41493  cdlemg20  41500  cdlemg22  41502  cdlemg24  41503  cdlemg37  41504  cdlemg31d  41515  cdlemg29  41520  cdlemg33b  41522  cdlemg33  41526  cdlemg38  41530  cdlemg39  41531  cdlemg40  41532  trlco  41542  trlcone  41543  cdlemg42  41544  cdlemg44b  41547  ltrncom  41553  trljco  41555  tendococl  41587  tendoplcl  41596  tendoplcom  41597  cdlemj2  41637  cdlemj3  41638  tendoid0  41640  tendoconid  41644  tendotr  41645  cdlemk25-3  41719  cdlemk26b-3  41720  cdlemk34  41725  cdlemk36  41728  cdlemk38  41730  cdlemkid4  41749  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk19x  41758  cdlemk53  41772  cdlemk55  41776  cdlemk55u  41781  cdlemk39u  41783  cdlemk19u  41785  cdlemk56  41786  tendoex  41790  cdleml3N  41793  cdleml5N  41795  tendospcanN  41838  cdlemm10N  41933  cdlemn11pre  42025  dihord2pre  42040  dihvalcqpre  42050  dihopelvalcpre  42063  dihord6apre  42071  dihord5b  42074  dihord5apre  42077  dihord  42079  dihmeetlem1N  42105  dihglblem5apreN  42106  dihglblem3N  42110  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetbN  42118  dihmeetlem4preN  42121  dihmeetlem5  42123  dihmeetlem7N  42125  dihmeetlem10N  42131  dihmeetlem11N  42132  dihmeetlem12N  42133  dihmeetlem13N  42134  dihmeetlem15N  42136  dihmeetlem16N  42137  dihmeetlem17N  42138  dihmeetlem18N  42139  dihmeetlem19N  42140  dihmeetALTN  42142  dih1dimatlem0  42143  dihlspsnssN  42147  dihlspsnat  42148  mapdh8ad  42594  hdmap14lem14  42696  hgmapvvlem3  42740  aks6d1c6isolem1  42982  dvdsexpnn  43135  resubcan2  43190  mzprename  43521  eldioph2lem1  43532  lzunuz  43540  rencldnfi  43589  pellexlem2  43598  infmrgelbi  43646  pellfundglb  43653  pellfund14gap  43655  qirropth  43676  rmxycomplete  43685  congadd  43734  acongeq  43751  jm2.19  43761  jm2.23  43764  jm2.20nn  43765  jm2.27  43776  jm3.1  43788  aomclem6  43827  lnmepi  43853  lmhmfgsplit  43854  lmhmlnmsplit  43855  pwssplit4  43857  hbtlem2  43892  hbtlem5  43896  dgraa0p  43917  proot1hash  43963  iocunico  43979  oasubex  44054  oege1  44074  relexpxpmin  44484  brtrclfv2  44494  ntrclsiso  44834  ntrclskb  44836  ntrclsk3  44837  k0004lem3  44916  grur1cld  44997  ismnu  45012  grumnudlem  45036  suprnmpt  45933  wessf1ornlem  45944  projf1o  45955  snunioo1  46269  iccintsng  46280  lptre2pt  46395  limcleqr  46399  fnlimfvre  46429  limsupgtlem  46532  volioc  46727  iblspltprt  46728  stoweidlem19  46774  stoweidlem20  46775  stoweidlem22  46777  stoweidlem28  46783  stoweidlem34  46789  stoweidlem44  46799  stoweidlem60  46815  wallispilem3  46822  fourierdlem41  46903  fourierdlem42  46904  fourierdlem49  46910  fourierdlem51  46912  fourierdlem54  46915  fourierdlem74  46935  fourierdlem97  46958  caratheodorylem2  47282  ovnsubaddlem2  47326  hspmbllem2  47382  smflimmpt  47565  smflimsupmpt  47584  smfliminfmpt  47587  funfocofob  47856  fzopredsuc  48102  nnmul2b  48109  imasetpreimafvbijlemfv  48192  iccpartigtl  48213  lighneal  48404  oexpnegALTV  48483  oexpnegnz  48484  tgblthelfgott  48621  clnbgrgrim  48740  uhgrimgrlim  48793  gpgusgralem  48862  lidldomn1  49037  ofaddmndmap  49164  lincdifsn  49245  lincellss  49247  lincresunit3lem3  49295  islindeps2  49304  lindssnlvec  49307  fdivmptf  49362  refdivmptf  49363  rrx2linest  49563  itsclc0yqsollem1  49583  itsclc0b  49593  itsclquadb  49597  itscnhlinecirc02plem3  49605  diag1  50123  setc1onsubc  50421