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  3593  2nreu  4402  predtrss  6318  frpomin  6336  f1prex  7284  cocan1  7291  weniso  7356  frrlem4  8291  frrlem10  8297  fprlem1  8302  smogt  8359  smocdmdom  8360  omeulem1  8574  nnmord  8625  nnmword  8626  naddasslem1  8688  naddasslem2  8689  difsnen  9062  enfixsn  9089  mapunen  9149  ac6sfi  9259  fissorduni  9266  fipreima  9331  elfiun  9406  ordiso2  9493  wemaplem2  9525  en2eqpr  10067  indcardi  10101  fodomfi2  10120  iunfictbso  10174  infmap2  10276  cofsmo  10328  cfsmolem  10329  coftr  10332  fin23lem11  10376  fincssdom  10382  fin23lem26  10384  isf32lem9  10420  ac6num  10538  gchdomtri  10695  gchpwdom  10736  winainflem  10759  tskuni  10849  gruima  10868  gruf  10877  grudomon  10883  elnpi  11054  distrlem4pr  11092  prlem934  11099  addcan  11475  addcan2  11476  divmulass  11978  divmulasscom  11979  ltmul1a  12147  suprleub  12264  supmul1  12267  suprzcl  12760  uzsupss  13048  xleadd1a  13364  xlesubadd  13374  xmulasslem3  13397  xlemul2a  13400  xadddilem  13405  xadddi2  13408  ixxun  13473  icoshftf1o  13586  ioounsn  13589  snunioc  13592  lincmb01cmp  13607  iccf1o  13608  nn0p1elfzo  13817  fzofzim  13824  fzoopth  13877  ltexp2a  14289  leexp2  14294  ltexp2r  14296  exple1  14300  expnlbnd2  14358  fun2dmnop0  14629  ccatass  14714  swrdswrdlem  14833  ccatopth  14845  repswpfx  14916  2cshw  14944  cshimadifsn  14960  cshimadifsn0  14961  cshco  14967  repsco  14971  s2f1o  15047  limsupgre  15628  addcn2  15741  mulcn2  15743  ntrivcvgmul  16051  binomrisefac  16188  dvdsmodexp  16410  dvdsadd2b  16456  dvdsexp2im  16477  dvdsmod  16479  oexpneg  16495  sadass  16621  gcdass  16700  rplpwr  16712  dvdsexpnn  16720  lcmfunsnlem1  16792  coprmdvds2  16809  rpmulgcd2  16811  qredeq  16812  rpdvds  16815  cncongr2  16823  rpexp  16878  prmdiveq  16943  hashgcdlem  16945  odzdvds  16953  modprmn0modprm0  16965  coprimeprodsq2  16967  pythagtriplem3  16976  pcdvdsb  17027  pcgcd1  17035  qexpz  17059  pockthg  17064  vdwnnlem1  17153  0ram  17178  ramz2  17182  lubss  18667  lubun  18669  clatleglb  18672  clatglbss  18673  mrelatglb  18714  isnsgrp  18892  issubmnd  18933  ress0gOLD  18935  mhmvlin  18976  gsumccat  19017  frmdss2  19039  submefmnd  19071  mulgneg  19282  mulgdirlem  19295  submmulg  19308  subgmulg  19331  nmzsubg  19355  ghmmulg  19422  gsmsymgreqlem1  19624  pmtrfb  19659  psgnunilem4  19691  odmodnn0  19734  odnncl  19739  odmod  19740  odmulgid  19748  odmulgeq  19751  odf1o1  19766  odf1o2  19767  odngen  19771  gexdvdsi  19777  pgpfi1  19789  odcau  19798  subgslw  19810  fislw  19819  lsmssv  19837  lsmless1x  19838  lsmless2x  19839  lsmsubm  19847  lsmmod  19869  lsmmod2  19870  efgred  19942  cntzcmn  20034  ghmplusg  20040  odadd1  20042  odadd2  20043  odadd  20044  lsmcomx  20050  gsumconst  20128  ablsimpgprmd  20311  ring1eq0  20509  mulgass2  20520  rngisom1  20676  rhmdvdsr  20738  isabvd  21049  rmodislmodlem  21184  rmodislmod  21185  lssintcl  21219  0lmhm  21295  lmhmvsca  21300  reslmhm2b  21309  pwssplit1  21314  pwssplit3  21316  lspfixed  21386  lspsnat  21403  unichnlidl  21496  pidlnz  21508  rnglidlrng  21515  2idlcpblrng  21545  lidldvgen  21638  xrsdsreclblem  21699  regsumsupp  21908  obselocv  22014  uvcresum  22079  frlmsslsp  22082  frlmup4  22087  lindff1  22106  f1lindf  22108  lsslindf  22116  islindf4  22124  lbslcic  22127  lindsenlbs  22137  issubassa  22155  evlsval2  22376  psrplusgpropd  22533  coe1subfv  22565  coe1mul2  22568  mpomatmul  22741  mamutpos  22753  scmatscmide  22802  mavmulsolcl  22846  marrepcl  22859  mdetdiag  22894  mdetunilem1  22907  mdetunilem3  22909  mdetunilem7  22913  mdetunilem9  22915  mdetmul  22918  slesolinvbi  22979  m2pmfzmap  23045  pmatcollpwlem  23078  pmatcollpw  23079  mp2pm2mplem4  23107  chpdmatlem3  23138  chfacfisfcpmat  23153  chfacfscmulgsum  23158  chfacfpmmulgsum  23162  chfacfpmmulgsum2  23163  cayhamlem1  23164  cpmidpmatlem2  23169  cpmadugsumlemB  23172  cpmadugsumlemC  23173  cpmadugsumlemF  23174  riinopn  23206  neiint  23402  topssnei  23422  restntr  23480  iscnp4  23561  cnconst2  23581  cnrest2  23584  cnprest2  23588  cnpdis  23591  cnt0  23644  cnt1  23648  cnhaus  23652  ordthauslem  23681  cncmp  23690  fiuncmp  23702  sscmp  23703  hauscmp  23705  cnconn  23720  unconn  23727  nlly2i  23775  llynlly  23776  nllyidm  23788  finlocfin  23819  ptrescn  23938  xkococnlem  23958  qtopss  24014  kqfvima  24029  r0cld  24037  ordthmeolem  24100  fbssint  24137  fmf  24244  fmss  24245  elfm  24246  rnelfmlem  24251  rnelfm  24252  fmco  24260  flimss2  24271  flimss1  24272  flimrest  24282  flftg  24295  cnpflf2  24299  cnpflf  24300  flfcnp  24303  supnfcls  24319  fclsss1  24321  fclsss2  24322  fcfnei  24334  fcfelbas  24335  cnpfcfi  24339  subgntr  24406  opnsubg  24407  cldsubg  24410  ghmcnp  24414  utop2nei  24549  neipcfilu  24594  bldisj  24697  blgt0  24698  bl2in  24699  blss2ps  24702  blss2  24703  blssps  24723  blss  24724  xmetresbl  24736  lpbl  24802  blcld  24804  stdbdbl  24816  metcnp3  24839  metcnp2  24841  txmetcnp  24846  blval2  24861  nmoix  25028  nmoeq0  25035  icoopnst  25240  iocopnst  25241  xrhmeo  25247  nmhmcn  25421  cphsqrtcl2  25487  cphsqrtcl3  25488  cfil3i  25570  caublcls  25610  bcthlem5  25629  cmetcusp1  25654  cssbn  25676  rrxcph  25693  pjth  25740  ovoliunlem2  25804  volun  25846  volsup2  25906  mbfimaopn2  25958  iblconst  26118  itgconst  26119  dvcnp2  26220  dvcn  26221  deg1mul3le  26415  deg1tmle  26416  dvdsq1p  26461  ig1peu  26473  ig1pdvds  26478  coeid3  26539  dgrmulc  26570  efcvx  26758  tanord  26848  logdivlti  26930  logccv  26973  recxpcl  26985  cxpeq  27067  ang180  27124  isosctrlem2  27129  cxp2lim  27286  amgm  27300  muval1  27442  dvdssqf  27447  mumullem2  27489  mumul  27490  bcmono  27586  lgsfcl2  27612  lgsdilem  27633  lgsdirprm  27640  lgsdir  27641  lgsdi  27643  lgsne0  27644  padicabv  27939  nosep1o  28020  nosep2o  28021  nosepssdm  28025  nolt02olem  28033  nosupres  28046  nosupbnd1lem1  28047  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd1lem6  28052  nosupbnd2  28055  noinfres  28061  noinfbnd1lem1  28062  noinfbnd1lem4  28065  noinfbnd1lem6  28067  noinfbnd2  28070  noetasuplem3  28074  noetalem1  28080  cutbdaybnd  28163  ltslpss  28276  leslss  28277  coinitslts  28287  addsass  28373  addsdi  28523  mulsass  28534  norecdiv  28558  bdayfinbndlem1  28835  z12bdaylem  28852  brbtwn2  29465  colinearalglem1  29466  colinearalg  29470  axcgrtr  29475  axsegconlem8  29484  axsegconlem9  29485  axsegconlem10  29486  axcontlem8  29531  axcontlem10  29533  elntg2  29545  vtxdlfuhgr1v  30042  umgr2wlk  30520  erclwwlksym  30594  clwwlkfo  30623  clwwlkext2edg  30629  erclwwlknsym  30643  clwwlknon1  30670  numclwwlk2lem1  30959  numclwwlk5  30971  frgrregord13  30979  nvmul0or  31234  ipval2lem2  31288  lnomul  31344  shless  31943  shlej1  31944  pjspansn  32161  hoadddi  32387  kbmul  32539  homco2  32561  kbass2  32701  eliccelico  33351  elicoelioo  33352  iocinioc2  33353  iocinif  33355  swrdrn2  33499  xrge0adddir  33561  xrge0npcan  33563  archiabl  33741  ress1r  33775  grplsm0l  33936  intlidl  33952  ssmxidl  33981  pstmfval  34510  fmcncfil  34545  zrhnm  34581  qqhnm  34604  measvunilem  34827  volfiniune  34845  dya2iocnrect  34896  sibfinima  34954  probun  35034  probinc  35036  cndprob01  35050  signstfvp  35183  bnj517  35498  bnj594  35525  pconnpi1  35971  cvmsss2  36008  mrsubcv  36244  msubvrs  36294  br6  36491  br4  36492  cgrcomim  36724  cgrtriv  36737  cgrextend  36743  segconeq  36745  btwntriv2  36747  btwnintr  36754  btwnexch3  36755  btwnouttr2  36757  trisegint  36763  cgrsub  36780  cgrxfr  36790  btwnxfr  36791  lineext  36811  btwnconn1lem13  36834  btwnconn1lem14  36835  btwnconn3  36838  segcon2  36840  brsegle  36843  brsegle2  36844  segletr  36849  segleantisym  36850  seglelin  36851  outsideofeu  36866  lineunray  36882  lineelsb2  36883  nmulss1  36933  ltnmul  36935  nmulle  36936  ltnadd  36937  naddle  36938  nadddi  36943  ivthALT  37093  weiunpo  37223  weiunso  37224  weiunfr  37225  weiunse  37226  areacirc  38599  cocanfo  38621  upixp  38631  ismtyima  38705  rrndstprj2  38733  zerdivemp1x  38849  lsatfixedN  40034  lssat  40041  eqlkr  40124  eqlkr2  40125  lkrlsp  40127  lshpkrlem4  40138  opposet  40206  cvrcon3b  40302  cvrcmp  40308  atlen0  40335  atnle  40342  atlatmstc  40344  cvlatexch3  40363  cvlsupr2  40368  hlsupr2  40412  hlrelat2  40428  cvrexchlem  40444  lnnat  40452  atcvrj2b  40457  atle  40461  atexchcvrN  40465  atbtwn  40471  athgt  40481  3dimlem3  40486  3dim1  40492  1cvratlt  40499  1cvrjat  40500  ps-1  40502  ps-2  40503  3atlem3  40510  3atlem5  40512  3atlem7  40514  llni  40533  llni2  40537  atcvrlln2  40544  llnexatN  40546  llncmp  40547  2llnmat  40549  2at0mat0  40550  lplni  40557  lplnnle2at  40566  2atnelpln  40569  lplnllnneN  40581  llncvrlpln2  40582  2lplnmN  40584  2llnmj  40585  lplncmp  40587  lplnexatN  40588  lplnexllnN  40589  2llnm3N  40594  lvoli  40600  lvoli3  40602  islvol2aN  40617  4atlem0a  40618  4atlem3  40621  4atlem3a  40622  4atlem4a  40624  4atlem4b  40625  4atlem4c  40626  4atlem4d  40627  4atlem10b  40630  4atlem11  40634  4atlem12  40637  lplncvrlvol2  40640  lvolcmp  40642  2lplnmj  40647  islinei  40765  pmapglbx  40794  linepmap  40800  lneq2at  40803  lnjatN  40805  lncvrat  40807  lncmp  40808  2llnma3r  40813  elpaddatriN  40828  elpaddat  40829  paddcom  40838  paddss1  40842  paddss2  40843  paddss12  40844  paddasslem6  40850  paddasslem7  40851  paddasslem8  40852  paddasslem9  40853  paddasslem15  40859  pmodlem2  40872  pmodl42N  40876  pmapjoin  40877  llnmod1i2  40885  2polcon4bN  40943  polcon2bN  40945  poml4N  40978  poml6N  40980  osumcllem1N  40981  osumcllem2N  40982  osumcllem11N  40991  osumclN  40992  pmapojoinN  40993  pexmidlem2N  40996  pexmidlem3N  40997  pexmidlem4N  40998  pexmidlem6N  41000  pexmidlem7N  41001  pl42lem2N  41005  pl42lem3N  41006  pl42lem4N  41007  pl42N  41008  lhpexle2lem  41034  lhpexle3lem  41036  lhpexle3  41037  lhpmcvr3  41050  lhp2at0nle  41060  lhprelat3N  41065  4atex  41101  4atex2  41102  lauteq  41120  lautco  41122  ltrncoidN  41153  ltrneq2  41173  ltrnnidn  41199  ltrnideq  41200  trlnid  41204  ltrnatlw  41208  trlnle  41211  trlval3  41212  trlval4  41213  cdlemc  41222  cdlemd5  41227  cdlemd9  41231  ltrneq3  41233  cdleme0moN  41250  cdleme20  41349  cdleme21j  41361  cdleme21  41362  cdleme27cl  41391  cdlemefrs29bpre0  41421  cdlemefs27cl  41438  cdlemefs32sn1aw  41439  cdleme43fsv1snlem  41445  cdleme32d  41469  cdleme32f  41471  cdleme32le  41472  cdleme35h2  41482  cdleme38n  41489  cdleme40m  41492  cdleme41snaw  41501  cdleme42ke  41510  cdleme17d3  41521  cdleme48fvg  41525  cdlemeg46fvcl  41531  cdlemeg46fgN  41559  cdleme48gfv1  41561  cdleme48fgv  41563  cdleme50trn3  41578  trlord  41594  ltrniotavalbN  41609  cdlemb3  41631  cdlemg6c  41645  cdlemg6  41648  cdlemg7N  41651  cdlemg8c  41654  cdlemg8  41656  cdlemg11a  41662  cdlemg11b  41667  cdlemg12e  41672  cdlemg15a  41680  cdlemg15  41681  cdlemg16  41682  cdlemg16z  41684  cdlemg16zz  41685  cdlemg17dN  41688  cdlemg18a  41703  cdlemg20  41710  cdlemg22  41712  cdlemg24  41713  cdlemg37  41714  cdlemg31d  41725  cdlemg29  41730  cdlemg33b  41732  cdlemg33  41736  cdlemg38  41740  cdlemg39  41741  cdlemg40  41742  trlco  41752  trlcone  41753  cdlemg42  41754  cdlemg44b  41757  ltrncom  41763  trljco  41765  tendococl  41797  tendoplcl  41806  tendoplcom  41807  cdlemj2  41847  cdlemj3  41848  tendoid0  41850  tendoconid  41854  tendotr  41855  cdlemk25-3  41929  cdlemk26b-3  41930  cdlemk34  41935  cdlemk36  41938  cdlemk38  41940  cdlemkid4  41959  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk19x  41968  cdlemk53  41982  cdlemk55  41986  cdlemk55u  41991  cdlemk39u  41993  cdlemk19u  41995  cdlemk56  41996  tendoex  42000  cdleml3N  42003  cdleml5N  42005  tendospcanN  42048  cdlemm10N  42143  cdlemn11pre  42235  dihord2pre  42250  dihvalcqpre  42260  dihopelvalcpre  42273  dihord6apre  42281  dihord5b  42284  dihord5apre  42287  dihord  42289  dihmeetlem1N  42315  dihglblem5apreN  42316  dihglblem3N  42320  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetbN  42328  dihmeetlem4preN  42331  dihmeetlem5  42333  dihmeetlem7N  42335  dihmeetlem10N  42341  dihmeetlem11N  42342  dihmeetlem12N  42343  dihmeetlem13N  42344  dihmeetlem15N  42346  dihmeetlem16N  42347  dihmeetlem17N  42348  dihmeetlem18N  42349  dihmeetlem19N  42350  dihmeetALTN  42352  dih1dimatlem0  42353  dihlspsnssN  42357  dihlspsnat  42358  mapdh8ad  42804  hdmap14lem14  42906  hgmapvvlem3  42950  aks6d1c6isolem1  43192  resubcan2  43407  mzprename  43713  eldioph2lem1  43724  lzunuz  43732  rencldnfi  43781  pellexlem2  43790  infmrgelbi  43838  pellfundglb  43845  pellfund14gap  43847  qirropth  43868  rmxycomplete  43877  congadd  43926  acongeq  43943  jm2.19  43953  jm2.23  43956  jm2.20nn  43957  jm2.27  43968  jm3.1  43980  aomclem6  44019  lnmepi  44045  lmhmfgsplit  44046  lmhmlnmsplit  44047  pwssplit4  44049  hbtlem2  44084  hbtlem5  44088  dgraa0p  44109  proot1hash  44155  iocunico  44171  oasubex  44246  oege1  44266  relexpxpmin  44676  brtrclfv2  44686  ntrclsiso  45026  ntrclskb  45028  ntrclsk3  45029  k0004lem3  45108  grur1cld  45189  ismnu  45204  grumnudlem  45228  suprnmpt  46132  wessf1ornlem  46143  projf1o  46154  snunioo1  46468  iccintsng  46479  lptre2pt  46594  limcleqr  46598  fnlimfvre  46628  limsupgtlem  46731  volioc  46926  iblspltprt  46927  stoweidlem19  46973  stoweidlem20  46974  stoweidlem22  46976  stoweidlem28  46982  stoweidlem34  46988  stoweidlem44  46998  stoweidlem60  47014  wallispilem3  47021  fourierdlem41  47102  fourierdlem42  47103  fourierdlem49  47109  fourierdlem51  47111  fourierdlem54  47114  fourierdlem74  47134  fourierdlem97  47157  caratheodorylem2  47481  ovnsubaddlem2  47525  hspmbllem2  47581  smflimmpt  47764  smflimsupmpt  47783  smfliminfmpt  47786  funfocofob  48092  fzopredsuc  48338  nnmul2b  48345  imasetpreimafvbijlemfv  48428  iccpartigtl  48449  lighneal  48640  oexpnegALTV  48719  oexpnegnz  48720  tgblthelfgott  48857  clnbgrgrim  48976  uhgrimgrlim  49029  gpgusgralem  49098  lidldomn1  49272  ofaddmndmap  49399  lincdifsn  49480  lincellss  49482  lincresunit3lem3  49530  islindeps2  49539  lindssnlvec  49542  fdivmptf  49597  refdivmptf  49598  rrx2linest  49798  itsclc0yqsollem1  49818  itsclc0b  49828  itsclquadb  49832  itscnhlinecirc02plem3  49840  diag1  50356  setc1onsubc  50654