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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpl11  1249  simpl21  1252  simpl31  1255  simp1l1  1267  simp2l1  1273  simp3l1  1279  3anandirs  1474  rspc3ev  3605  2nreu  4407  predtrss  6295  frpomin  6313  f1prex  7259  cocan1  7266  weniso  7329  frrlem4  8268  frrlem10  8274  fprlem1  8279  smogt  8336  smocdmdom  8337  omeulem1  8546  nnmord  8596  nnmword  8597  naddasslem1  8658  naddasslem2  8659  difsnen  9023  enfixsn  9050  mapunen  9110  ac6sfi  9231  fipreima  9309  elfiun  9381  ordiso2  9468  wemaplem2  9500  en2eqpr  9960  indcardi  9994  fodomfi2  10013  iunfictbso  10067  infmap2  10170  cofsmo  10222  cfsmolem  10223  coftr  10226  fin23lem11  10270  fincssdom  10276  fin23lem26  10278  isf32lem9  10314  ac6num  10432  gchdomtri  10582  gchpwdom  10623  winainflem  10646  tskuni  10736  gruima  10755  gruf  10764  grudomon  10770  elnpi  10941  distrlem4pr  10979  prlem934  10986  addcan  11358  addcan2  11359  divmulass  11860  divmulasscom  11861  ltmul1a  12031  suprleub  12149  supmul1  12152  suprzcl  12614  uzsupss  12899  xleadd1a  13213  xlesubadd  13223  xmulasslem3  13246  xlemul2a  13249  xadddilem  13254  xadddi2  13257  ixxun  13322  icoshftf1o  13435  ioounsn  13438  snunioc  13441  lincmb01cmp  13456  iccf1o  13457  nn0p1elfzo  13663  fzofzim  13670  fzoopth  13723  ltexp2a  14131  leexp2  14136  ltexp2r  14138  exple1  14142  expnlbnd2  14199  fun2dmnop0  14469  ccatass  14553  swrdswrdlem  14669  ccatopth  14681  repswpfx  14750  2cshw  14778  cshimadifsn  14795  cshimadifsn0  14796  cshco  14802  repsco  14806  s2f1o  14882  limsupgre  15447  addcn2  15560  mulcn2  15562  ntrivcvgmul  15868  binomrisefac  16008  dvdsmodexp  16230  dvdsadd2b  16276  dvdsexp2im  16297  dvdsmod  16299  oexpneg  16315  sadass  16441  gcdass  16517  rplpwr  16528  lcmfunsnlem1  16607  coprmdvds2  16624  rpmulgcd2  16626  qredeq  16627  rpdvds  16630  cncongr2  16638  rpexp  16692  prmdiveq  16756  hashgcdlem  16758  odzdvds  16766  modprmn0modprm0  16778  coprimeprodsq2  16780  pythagtriplem3  16789  pcdvdsb  16840  pcgcd1  16848  qexpz  16872  pockthg  16877  vdwnnlem1  16966  0ram  16991  ramz2  16995  lubss  18472  lubun  18474  clatleglb  18477  clatglbss  18478  mrelatglb  18519  isnsgrp  18650  issubmnd  18688  ress0g  18689  mhmvlin  18728  gsumccat  18768  frmdss2  18790  submefmnd  18822  mulgneg  19024  mulgdirlem  19037  submmulg  19050  subgmulg  19072  nmzsubg  19097  ghmmulg  19160  gsmsymgreqlem1  19360  pmtrfb  19395  psgnunilem4  19427  odmodnn0  19470  odnncl  19475  odmod  19476  odmulgid  19484  odmulgeq  19487  odf1o1  19502  odf1o2  19503  odngen  19507  gexdvdsi  19513  pgpfi1  19525  odcau  19534  subgslw  19546  fislw  19555  lsmssv  19573  lsmless1x  19574  lsmless2x  19575  lsmsubm  19583  lsmmod  19605  lsmmod2  19606  efgred  19678  cntzcmn  19770  ghmplusg  19776  odadd1  19778  odadd2  19779  odadd  19780  lsmcomx  19786  gsumconst  19864  ablsimpgprmd  20047  srg1zr  20124  ring1eq0  20207  mulgass2  20218  rngisom1  20375  rhmdvdsr  20417  isabvd  20721  rmodislmodlem  20835  rmodislmod  20836  lssintcl  20870  0lmhm  20947  lmhmvsca  20952  reslmhm2b  20961  pwssplit1  20966  pwssplit3  20968  lspfixed  21038  lspsnat  21055  rnglidlrng  21157  2idlcpblrng  21181  lidldvgen  21244  xrsdsreclblem  21329  regsumsupp  21531  obselocv  21637  uvcresum  21702  frlmsslsp  21705  frlmup4  21710  lindff1  21729  f1lindf  21731  lsslindf  21739  islindf4  21747  lbslcic  21750  issubassa  21776  evlsval2  21994  psrplusgpropd  22120  coe1subfv  22152  coe1mul2  22155  mpomatmul  22333  mamutpos  22345  scmatscmide  22394  mavmulsolcl  22438  marrepcl  22451  mdetdiag  22486  mdetunilem1  22499  mdetunilem3  22501  mdetunilem7  22505  mdetunilem9  22507  mdetmul  22510  slesolinvbi  22568  m2pmfzmap  22634  pmatcollpwlem  22667  pmatcollpw  22668  mp2pm2mplem4  22696  chpdmatlem3  22727  chfacfisfcpmat  22742  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmidpmatlem2  22758  cpmadugsumlemB  22761  cpmadugsumlemC  22762  cpmadugsumlemF  22763  riinopn  22795  neiint  22991  topssnei  23011  restntr  23069  iscnp4  23150  cnconst2  23170  cnrest2  23173  cnprest2  23177  cnpdis  23180  cnt0  23233  cnt1  23237  cnhaus  23241  ordthauslem  23270  cncmp  23279  fiuncmp  23291  sscmp  23292  hauscmp  23294  cnconn  23309  unconn  23316  nlly2i  23363  llynlly  23364  nllyidm  23376  finlocfin  23407  ptrescn  23526  xkococnlem  23546  qtopss  23602  kqfvima  23617  r0cld  23625  ordthmeolem  23688  fbssint  23725  fmf  23832  fmss  23833  elfm  23834  rnelfmlem  23839  rnelfm  23840  fmco  23848  flimss2  23859  flimss1  23860  flimrest  23870  flftg  23883  cnpflf2  23887  cnpflf  23888  flfcnp  23891  supnfcls  23907  fclsss1  23909  fclsss2  23910  fcfnei  23922  fcfelbas  23923  cnpfcfi  23927  subgntr  23994  opnsubg  23995  cldsubg  23998  ghmcnp  24002  utop2nei  24138  neipcfilu  24183  bldisj  24286  blgt0  24287  bl2in  24288  blss2ps  24291  blss2  24292  blssps  24312  blss  24313  xmetresbl  24325  lpbl  24391  blcld  24393  stdbdbl  24405  metcnp3  24428  metcnp2  24430  txmetcnp  24435  blval2  24450  nmoix  24617  nmoeq0  24624  icoopnst  24836  iocopnst  24837  xrhmeo  24844  nmhmcn  25020  cphsqrtcl2  25086  cphsqrtcl3  25087  cfil3i  25169  caublcls  25209  bcthlem5  25228  cmetcusp1  25253  cssbn  25275  rrxcph  25292  pjth  25339  ovoliunlem2  25404  volun  25446  volsup2  25506  mbfimaopn2  25558  iblconst  25719  itgconst  25720  dvcnp2  25821  dvcnp2OLD  25822  dvcn  25823  deg1mul3le  26022  deg1tmle  26023  dvdsq1p  26068  ig1peu  26080  ig1pdvds  26085  coeid3  26145  dgrmulc  26177  efcvx  26359  tanord  26447  logdivlti  26529  logccv  26572  recxpcl  26584  cxpeq  26667  ang180  26724  isosctrlem2  26729  cxp2lim  26887  amgm  26901  muval1  27043  dvdssqf  27048  mumullem2  27090  mumul  27091  bcmono  27188  lgsfcl2  27214  lgsdilem  27235  lgsdirprm  27242  lgsdir  27243  lgsdi  27245  lgsne0  27246  padicabv  27541  nosep1o  27593  nosep2o  27594  nosepssdm  27598  nolt02olem  27606  nosupres  27619  nosupbnd1lem1  27620  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  nosupbnd2  27628  noinfres  27634  noinfbnd1lem1  27635  noinfbnd1lem4  27638  noinfbnd1lem6  27640  noinfbnd2  27643  noetasuplem3  27647  noetalem1  27653  scutbdaybnd  27727  sltlpss  27819  slelss  27820  coinitsslt  27827  addsass  27912  addsdi  28058  mulsass  28069  norecdiv  28093  brbtwn2  28832  colinearalglem1  28833  colinearalg  28837  axcgrtr  28842  axsegconlem8  28851  axsegconlem9  28852  axsegconlem10  28853  axcontlem8  28898  axcontlem10  28900  elntg2  28912  vtxdlfuhgr1v  29407  umgr2wlk  29879  erclwwlksym  29950  clwwlkfo  29979  clwwlkext2edg  29985  erclwwlknsym  29999  clwwlknon1  30026  numclwwlk2lem1  30305  numclwwlk5  30317  frgrregord13  30325  nvmul0or  30579  ipval2lem2  30633  lnomul  30689  shless  31288  shlej1  31289  pjspansn  31506  hoadddi  31732  kbmul  31884  homco2  31906  kbass2  32046  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  iocinif  32704  swrdrn2  32876  xrge0adddir  32959  xrge0npcan  32961  archiabl  33152  ress1r  33185  pidlnz  33347  grplsm0l  33374  intlidl  33391  ssmxidl  33445  pstmfval  33886  fmcncfil  33921  zrhnm  33957  qqhnm  33980  measvunilem  34202  volfiniune  34220  dya2iocnrect  34272  sibfinima  34330  probun  34410  probinc  34412  cndprob01  34426  signstfvp  34562  bnj517  34875  bnj594  34902  pconnpi1  35224  cvmsss2  35261  mrsubcv  35497  msubvrs  35547  br6  35744  br4  35745  cgrcomim  35977  cgrtriv  35990  cgrextend  35996  segconeq  35998  btwntriv2  36000  btwnintr  36007  btwnexch3  36008  btwnouttr2  36010  trisegint  36016  cgrsub  36033  cgrxfr  36043  btwnxfr  36044  lineext  36064  btwnconn1lem13  36087  btwnconn1lem14  36088  btwnconn3  36091  segcon2  36093  brsegle  36096  brsegle2  36097  segletr  36102  segleantisym  36103  seglelin  36104  outsideofeu  36119  lineunray  36135  lineelsb2  36136  ivthALT  36323  weiunpo  36453  weiunso  36454  weiunfr  36455  weiunse  36456  lindsenlbs  37609  areacirc  37707  cocanfo  37713  upixp  37723  ismtyima  37797  rrndstprj2  37825  zerdivemp1x  37941  lsatfixedN  39002  lssat  39009  eqlkr  39092  eqlkr2  39093  lkrlsp  39095  lshpkrlem4  39106  opposet  39174  cvrcon3b  39270  cvrcmp  39276  atlen0  39303  atnle  39310  atlatmstc  39312  cvlatexch3  39331  cvlsupr2  39336  hlsupr2  39381  hlrelat2  39397  cvrexchlem  39413  lnnat  39421  atcvrj2b  39426  atle  39430  atexchcvrN  39434  atbtwn  39440  athgt  39450  3dimlem3  39455  3dim1  39461  1cvratlt  39468  1cvrjat  39469  ps-1  39471  ps-2  39472  3atlem3  39479  3atlem5  39481  3atlem7  39483  llni  39502  llni2  39506  atcvrlln2  39513  llnexatN  39515  llncmp  39516  2llnmat  39518  2at0mat0  39519  lplni  39526  lplnnle2at  39535  2atnelpln  39538  lplnllnneN  39550  llncvrlpln2  39551  2lplnmN  39553  2llnmj  39554  lplncmp  39556  lplnexatN  39557  lplnexllnN  39558  2llnm3N  39563  lvoli  39569  lvoli3  39571  islvol2aN  39586  4atlem0a  39587  4atlem3  39590  4atlem3a  39591  4atlem4a  39593  4atlem4b  39594  4atlem4c  39595  4atlem4d  39596  4atlem10b  39599  4atlem11  39603  4atlem12  39606  lplncvrlvol2  39609  lvolcmp  39611  2lplnmj  39616  islinei  39734  pmapglbx  39763  linepmap  39769  lneq2at  39772  lnjatN  39774  lncvrat  39776  lncmp  39777  2llnma3r  39782  elpaddatriN  39797  elpaddat  39798  paddcom  39807  paddss1  39811  paddss2  39812  paddss12  39813  paddasslem6  39819  paddasslem7  39820  paddasslem8  39821  paddasslem9  39822  paddasslem15  39828  pmodlem2  39841  pmodl42N  39845  pmapjoin  39846  llnmod1i2  39854  2polcon4bN  39912  polcon2bN  39914  poml4N  39947  poml6N  39949  osumcllem1N  39950  osumcllem2N  39951  osumcllem11N  39960  osumclN  39961  pmapojoinN  39962  pexmidlem2N  39965  pexmidlem3N  39966  pexmidlem4N  39967  pexmidlem6N  39969  pexmidlem7N  39970  pl42lem2N  39974  pl42lem3N  39975  pl42lem4N  39976  pl42N  39977  lhpexle2lem  40003  lhpexle3lem  40005  lhpexle3  40006  lhpmcvr3  40019  lhp2at0nle  40029  lhprelat3N  40034  4atex  40070  4atex2  40071  lauteq  40089  lautco  40091  ltrncoidN  40122  ltrneq2  40142  ltrnnidn  40168  ltrnideq  40169  trlnid  40173  ltrnatlw  40177  trlnle  40180  trlval3  40181  trlval4  40182  cdlemc  40191  cdlemd5  40196  cdlemd9  40200  ltrneq3  40202  cdleme0moN  40219  cdleme20  40318  cdleme21j  40330  cdleme21  40331  cdleme27cl  40360  cdlemefrs29bpre0  40390  cdlemefs27cl  40407  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme32d  40438  cdleme32f  40440  cdleme32le  40441  cdleme35h2  40451  cdleme38n  40458  cdleme40m  40461  cdleme41snaw  40470  cdleme42ke  40479  cdleme17d3  40490  cdleme48fvg  40494  cdlemeg46fvcl  40500  cdlemeg46fgN  40528  cdleme48gfv1  40530  cdleme48fgv  40532  cdleme50trn3  40547  trlord  40563  ltrniotavalbN  40578  cdlemb3  40600  cdlemg6c  40614  cdlemg6  40617  cdlemg7N  40620  cdlemg8c  40623  cdlemg8  40625  cdlemg11a  40631  cdlemg11b  40636  cdlemg12e  40641  cdlemg15a  40649  cdlemg15  40650  cdlemg16  40651  cdlemg16z  40653  cdlemg16zz  40654  cdlemg17dN  40657  cdlemg18a  40672  cdlemg20  40679  cdlemg22  40681  cdlemg24  40682  cdlemg37  40683  cdlemg31d  40694  cdlemg29  40699  cdlemg33b  40701  cdlemg33  40705  cdlemg38  40709  cdlemg39  40710  cdlemg40  40711  trlco  40721  trlcone  40722  cdlemg42  40723  cdlemg44b  40726  ltrncom  40732  trljco  40734  tendococl  40766  tendoplcl  40775  tendoplcom  40776  cdlemj2  40816  cdlemj3  40817  tendoid0  40819  tendoconid  40823  tendotr  40824  cdlemk25-3  40898  cdlemk26b-3  40899  cdlemk34  40904  cdlemk36  40907  cdlemk38  40909  cdlemkid4  40928  cdlemk35s-id  40932  cdlemk39s-id  40934  cdlemk19x  40937  cdlemk53  40951  cdlemk55  40955  cdlemk55u  40960  cdlemk39u  40962  cdlemk19u  40964  cdlemk56  40965  tendoex  40969  cdleml3N  40972  cdleml5N  40974  tendospcanN  41017  cdlemm10N  41112  cdlemn11pre  41204  dihord2pre  41219  dihvalcqpre  41229  dihopelvalcpre  41242  dihord6apre  41250  dihord5b  41253  dihord5apre  41256  dihord  41258  dihmeetlem1N  41284  dihglblem5apreN  41285  dihglblem3N  41289  dihmeetlem2N  41293  dihglbcpreN  41294  dihmeetbN  41297  dihmeetlem4preN  41300  dihmeetlem5  41302  dihmeetlem7N  41304  dihmeetlem10N  41310  dihmeetlem11N  41311  dihmeetlem12N  41312  dihmeetlem13N  41313  dihmeetlem15N  41315  dihmeetlem16N  41316  dihmeetlem17N  41317  dihmeetlem18N  41318  dihmeetlem19N  41319  dihmeetALTN  41321  dih1dimatlem0  41322  dihlspsnssN  41326  dihlspsnat  41327  mapdh8ad  41773  hdmap14lem14  41875  hgmapvvlem3  41919  aks6d1c6isolem1  42162  dvdsexpnn  42321  resubcan2  42376  mzprename  42737  eldioph2lem1  42748  lzunuz  42756  rencldnfi  42809  pellexlem2  42818  infmrgelbi  42866  pellfundglb  42873  pellfund14gap  42875  qirropth  42896  rmxycomplete  42906  congadd  42955  acongeq  42972  jm2.19  42982  jm2.23  42985  jm2.20nn  42986  jm2.27  42997  jm3.1  43009  aomclem6  43048  lnmepi  43074  lmhmfgsplit  43075  lmhmlnmsplit  43076  pwssplit4  43078  hbtlem2  43113  hbtlem5  43117  dgraa0p  43138  proot1hash  43184  iocunico  43200  oasubex  43275  oege1  43295  relexpxpmin  43706  brtrclfv2  43716  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  k0004lem3  44138  grur1cld  44221  ismnu  44250  grumnudlem  44274  suprnmpt  45168  wessf1ornlem  45179  projf1o  45191  snunioo1  45510  iccintsng  45521  lptre2pt  45638  limcleqr  45642  fnlimfvre  45672  limsupgtlem  45775  volioc  45970  iblspltprt  45971  stoweidlem19  46017  stoweidlem20  46018  stoweidlem22  46020  stoweidlem28  46026  stoweidlem34  46032  stoweidlem44  46042  stoweidlem60  46058  wallispilem3  46065  fourierdlem41  46146  fourierdlem42  46147  fourierdlem49  46153  fourierdlem51  46155  fourierdlem54  46158  fourierdlem74  46178  fourierdlem97  46201  caratheodorylem2  46525  ovnsubaddlem2  46569  hspmbllem2  46625  smflimmpt  46808  smflimsupmpt  46827  smfliminfmpt  46830  funfocofob  47079  fzopredsuc  47324  imasetpreimafvbijlemfv  47403  iccpartigtl  47424  lighneal  47612  oexpnegALTV  47678  oexpnegnz  47679  tgblthelfgott  47816  clnbgrgrim  47934  uhgrimgrlim  47986  gpgusgralem  48047  lidldomn1  48219  ofaddmndmap  48331  lincdifsn  48413  lincellss  48415  lincresunit3lem3  48463  islindeps2  48472  lindssnlvec  48475  fdivmptf  48530  refdivmptf  48531  rrx2linest  48731  itsclc0yqsollem1  48751  itsclc0b  48761  itsclquadb  48765  itscnhlinecirc02plem3  48773  diag1  49293  setc1onsubc  49591