Theorem simpl1 1193

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 1187	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

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

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 1089

This theorem is referenced by:  simpl11  1250  simpl21  1253  simpl31  1256  simp1l1  1268  simp2l1  1274  simp3l1  1280  3anandirs  1475  rspc3ev  3581  2nreu  4384  predtrss  6286  frpomin  6304  f1prex  7239  cocan1  7246  weniso  7309  frrlem4  8239  frrlem10  8245  fprlem1  8250  smogt  8307  smocdmdom  8308  omeulem1  8517  nnmord  8568  nnmword  8569  naddasslem1  8630  naddasslem2  8631  difsnen  8997  enfixsn  9024  mapunen  9084  ac6sfi  9194  fipreima  9268  elfiun  9343  ordiso2  9430  wemaplem2  9462  en2eqpr  9929  indcardi  9963  fodomfi2  9982  iunfictbso  10036  infmap2  10139  cofsmo  10191  cfsmolem  10192  coftr  10195  fin23lem11  10239  fincssdom  10245  fin23lem26  10247  isf32lem9  10283  ac6num  10401  gchdomtri  10552  gchpwdom  10593  winainflem  10616  tskuni  10706  gruima  10725  gruf  10734  grudomon  10740  elnpi  10911  distrlem4pr  10949  prlem934  10956  addcan  11330  addcan2  11331  divmulass  11832  divmulasscom  11833  ltmul1a  12004  suprleub  12122  supmul1  12125  suprzcl  12609  uzsupss  12890  xleadd1a  13205  xlesubadd  13215  xmulasslem3  13238  xlemul2a  13241  xadddilem  13246  xadddi2  13249  ixxun  13314  icoshftf1o  13427  ioounsn  13430  snunioc  13433  lincmb01cmp  13448  iccf1o  13449  nn0p1elfzo  13657  fzofzim  13664  fzoopth  13717  ltexp2a  14128  leexp2  14133  ltexp2r  14135  exple1  14139  expnlbnd2  14196  fun2dmnop0  14466  ccatass  14551  swrdswrdlem  14666  ccatopth  14678  repswpfx  14747  2cshw  14775  cshimadifsn  14791  cshimadifsn0  14792  cshco  14798  repsco  14802  s2f1o  14878  limsupgre  15443  addcn2  15556  mulcn2  15558  ntrivcvgmul  15867  binomrisefac  16007  dvdsmodexp  16229  dvdsadd2b  16275  dvdsexp2im  16296  dvdsmod  16298  oexpneg  16314  sadass  16440  gcdass  16516  rplpwr  16527  lcmfunsnlem1  16606  coprmdvds2  16623  rpmulgcd2  16625  qredeq  16626  rpdvds  16629  cncongr2  16637  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  18479  lubun  18481  clatleglb  18484  clatglbss  18485  mrelatglb  18526  isnsgrp  18691  issubmnd  18729  ress0g  18730  mhmvlin  18769  gsumccat  18809  frmdss2  18831  submefmnd  18863  mulgneg  19068  mulgdirlem  19081  submmulg  19094  subgmulg  19116  nmzsubg  19140  ghmmulg  19203  gsmsymgreqlem1  19405  pmtrfb  19440  psgnunilem4  19472  odmodnn0  19515  odnncl  19520  odmod  19521  odmulgid  19529  odmulgeq  19532  odf1o1  19547  odf1o2  19548  odngen  19552  gexdvdsi  19558  pgpfi1  19570  odcau  19579  subgslw  19591  fislw  19600  lsmssv  19618  lsmless1x  19619  lsmless2x  19620  lsmsubm  19628  lsmmod  19650  lsmmod2  19651  efgred  19723  cntzcmn  19815  ghmplusg  19821  odadd1  19823  odadd2  19824  odadd  19825  lsmcomx  19831  gsumconst  19909  ablsimpgprmd  20092  srg1zr  20196  ring1eq0  20279  mulgass2  20290  rngisom1  20446  rhmdvdsr  20485  isabvd  20789  rmodislmodlem  20924  rmodislmod  20925  lssintcl  20959  0lmhm  21035  lmhmvsca  21040  reslmhm2b  21049  pwssplit1  21054  pwssplit3  21056  lspfixed  21126  lspsnat  21143  rnglidlrng  21245  2idlcpblrng  21269  lidldvgen  21332  xrsdsreclblem  21393  regsumsupp  21602  obselocv  21708  uvcresum  21773  frlmsslsp  21776  frlmup4  21781  lindff1  21800  f1lindf  21802  lsslindf  21810  islindf4  21818  lbslcic  21821  issubassa  21847  evlsval2  22065  psrplusgpropd  22199  coe1subfv  22231  coe1mul2  22234  mpomatmul  22411  mamutpos  22423  scmatscmide  22472  mavmulsolcl  22516  marrepcl  22529  mdetdiag  22564  mdetunilem1  22577  mdetunilem3  22579  mdetunilem7  22583  mdetunilem9  22585  mdetmul  22588  slesolinvbi  22646  m2pmfzmap  22712  pmatcollpwlem  22745  pmatcollpw  22746  mp2pm2mplem4  22774  chpdmatlem3  22805  chfacfisfcpmat  22820  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  chfacfpmmulgsum2  22830  cayhamlem1  22831  cpmidpmatlem2  22836  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  riinopn  22873  neiint  23069  topssnei  23089  restntr  23147  iscnp4  23228  cnconst2  23248  cnrest2  23251  cnprest2  23255  cnpdis  23258  cnt0  23311  cnt1  23315  cnhaus  23319  ordthauslem  23348  cncmp  23357  fiuncmp  23369  sscmp  23370  hauscmp  23372  cnconn  23387  unconn  23394  nlly2i  23441  llynlly  23442  nllyidm  23454  finlocfin  23485  ptrescn  23604  xkococnlem  23624  qtopss  23680  kqfvima  23695  r0cld  23703  ordthmeolem  23766  fbssint  23803  fmf  23910  fmss  23911  elfm  23912  rnelfmlem  23917  rnelfm  23918  fmco  23926  flimss2  23937  flimss1  23938  flimrest  23948  flftg  23961  cnpflf2  23965  cnpflf  23966  flfcnp  23969  supnfcls  23985  fclsss1  23987  fclsss2  23988  fcfnei  24000  fcfelbas  24001  cnpfcfi  24005  subgntr  24072  opnsubg  24073  cldsubg  24076  ghmcnp  24080  utop2nei  24215  neipcfilu  24260  bldisj  24363  blgt0  24364  bl2in  24365  blss2ps  24368  blss2  24369  blssps  24389  blss  24390  xmetresbl  24402  lpbl  24468  blcld  24470  stdbdbl  24482  metcnp3  24505  metcnp2  24507  txmetcnp  24512  blval2  24527  nmoix  24694  nmoeq0  24701  icoopnst  24906  iocopnst  24907  xrhmeo  24913  nmhmcn  25087  cphsqrtcl2  25153  cphsqrtcl3  25154  cfil3i  25236  caublcls  25276  bcthlem5  25295  cmetcusp1  25320  cssbn  25342  rrxcph  25359  pjth  25406  ovoliunlem2  25470  volun  25512  volsup2  25572  mbfimaopn2  25624  iblconst  25785  itgconst  25786  dvcnp2  25887  dvcn  25888  deg1mul3le  26082  deg1tmle  26083  dvdsq1p  26128  ig1peu  26140  ig1pdvds  26145  coeid3  26205  dgrmulc  26236  efcvx  26414  tanord  26502  logdivlti  26584  logccv  26627  recxpcl  26639  cxpeq  26721  ang180  26778  isosctrlem2  26783  cxp2lim  26940  amgm  26954  muval1  27096  dvdssqf  27101  mumullem2  27143  mumul  27144  bcmono  27240  lgsfcl2  27266  lgsdilem  27287  lgsdirprm  27294  lgsdir  27295  lgsdi  27297  lgsne0  27298  padicabv  27593  nosep1o  27645  nosep2o  27646  nosepssdm  27650  nolt02olem  27658  nosupres  27671  nosupbnd1lem1  27672  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  nosupbnd2  27680  noinfres  27686  noinfbnd1lem1  27687  noinfbnd1lem4  27690  noinfbnd1lem6  27692  noinfbnd2  27695  noetasuplem3  27699  noetalem1  27705  cutbdaybnd  27787  ltslpss  27900  leslss  27901  coinitslts  27911  addsass  27997  addsdi  28147  mulsass  28158  norecdiv  28182  bdayfinbndlem1  28459  z12bdaylem  28476  brbtwn2  28974  colinearalglem1  28975  colinearalg  28979  axcgrtr  28984  axsegconlem8  28993  axsegconlem9  28994  axsegconlem10  28995  axcontlem8  29040  axcontlem10  29042  elntg2  29054  vtxdlfuhgr1v  29548  umgr2wlk  30017  erclwwlksym  30091  clwwlkfo  30120  clwwlkext2edg  30126  erclwwlknsym  30140  clwwlknon1  30167  numclwwlk2lem1  30446  numclwwlk5  30458  frgrregord13  30466  nvmul0or  30721  ipval2lem2  30775  lnomul  30831  shless  31430  shlej1  31431  pjspansn  31648  hoadddi  31874  kbmul  32026  homco2  32048  kbass2  32188  eliccelico  32850  elicoelioo  32851  iocinioc2  32852  iocinif  32854  swrdrn2  33014  xrge0adddir  33078  xrge0npcan  33080  archiabl  33259  ress1r  33294  pidlnz  33436  grplsm0l  33463  intlidl  33480  ssmxidl  33534  pstmfval  34040  fmcncfil  34075  zrhnm  34111  qqhnm  34134  measvunilem  34356  volfiniune  34374  dya2iocnrect  34425  sibfinima  34483  probun  34563  probinc  34565  cndprob01  34579  signstfvp  34715  bnj517  35027  bnj594  35054  fissorduni  35233  pconnpi1  35419  cvmsss2  35456  mrsubcv  35692  msubvrs  35742  br6  35939  br4  35940  cgrcomim  36171  cgrtriv  36184  cgrextend  36190  segconeq  36192  btwntriv2  36194  btwnintr  36201  btwnexch3  36202  btwnouttr2  36204  trisegint  36210  cgrsub  36227  cgrxfr  36237  btwnxfr  36238  lineext  36258  btwnconn1lem13  36281  btwnconn1lem14  36282  btwnconn3  36285  segcon2  36287  brsegle  36290  brsegle2  36291  segletr  36296  segleantisym  36297  seglelin  36298  outsideofeu  36313  lineunray  36329  lineelsb2  36330  ivthALT  36517  weiunpo  36647  weiunso  36648  weiunfr  36649  weiunse  36650  lindsenlbs  37936  areacirc  38034  cocanfo  38040  upixp  38050  ismtyima  38124  rrndstprj2  38152  zerdivemp1x  38268  lsatfixedN  39455  lssat  39462  eqlkr  39545  eqlkr2  39546  lkrlsp  39548  lshpkrlem4  39559  opposet  39627  cvrcon3b  39723  cvrcmp  39729  atlen0  39756  atnle  39763  atlatmstc  39765  cvlatexch3  39784  cvlsupr2  39789  hlsupr2  39833  hlrelat2  39849  cvrexchlem  39865  lnnat  39873  atcvrj2b  39878  atle  39882  atexchcvrN  39886  atbtwn  39892  athgt  39902  3dimlem3  39907  3dim1  39913  1cvratlt  39920  1cvrjat  39921  ps-1  39923  ps-2  39924  3atlem3  39931  3atlem5  39933  3atlem7  39935  llni  39954  llni2  39958  atcvrlln2  39965  llnexatN  39967  llncmp  39968  2llnmat  39970  2at0mat0  39971  lplni  39978  lplnnle2at  39987  2atnelpln  39990  lplnllnneN  40002  llncvrlpln2  40003  2lplnmN  40005  2llnmj  40006  lplncmp  40008  lplnexatN  40009  lplnexllnN  40010  2llnm3N  40015  lvoli  40021  lvoli3  40023  islvol2aN  40038  4atlem0a  40039  4atlem3  40042  4atlem3a  40043  4atlem4a  40045  4atlem4b  40046  4atlem4c  40047  4atlem4d  40048  4atlem10b  40051  4atlem11  40055  4atlem12  40058  lplncvrlvol2  40061  lvolcmp  40063  2lplnmj  40068  islinei  40186  pmapglbx  40215  linepmap  40221  lneq2at  40224  lnjatN  40226  lncvrat  40228  lncmp  40229  2llnma3r  40234  elpaddatriN  40249  elpaddat  40250  paddcom  40259  paddss1  40263  paddss2  40264  paddss12  40265  paddasslem6  40271  paddasslem7  40272  paddasslem8  40273  paddasslem9  40274  paddasslem15  40280  pmodlem2  40293  pmodl42N  40297  pmapjoin  40298  llnmod1i2  40306  2polcon4bN  40364  polcon2bN  40366  poml4N  40399  poml6N  40401  osumcllem1N  40402  osumcllem2N  40403  osumcllem11N  40412  osumclN  40413  pmapojoinN  40414  pexmidlem2N  40417  pexmidlem3N  40418  pexmidlem4N  40419  pexmidlem6N  40421  pexmidlem7N  40422  pl42lem2N  40426  pl42lem3N  40427  pl42lem4N  40428  pl42N  40429  lhpexle2lem  40455  lhpexle3lem  40457  lhpexle3  40458  lhpmcvr3  40471  lhp2at0nle  40481  lhprelat3N  40486  4atex  40522  4atex2  40523  lauteq  40541  lautco  40543  ltrncoidN  40574  ltrneq2  40594  ltrnnidn  40620  ltrnideq  40621  trlnid  40625  ltrnatlw  40629  trlnle  40632  trlval3  40633  trlval4  40634  cdlemc  40643  cdlemd5  40648  cdlemd9  40652  ltrneq3  40654  cdleme0moN  40671  cdleme20  40770  cdleme21j  40782  cdleme21  40783  cdleme27cl  40812  cdlemefrs29bpre0  40842  cdlemefs27cl  40859  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme32d  40890  cdleme32f  40892  cdleme32le  40893  cdleme35h2  40903  cdleme38n  40910  cdleme40m  40913  cdleme41snaw  40922  cdleme42ke  40931  cdleme17d3  40942  cdleme48fvg  40946  cdlemeg46fvcl  40952  cdlemeg46fgN  40980  cdleme48gfv1  40982  cdleme48fgv  40984  cdleme50trn3  40999  trlord  41015  ltrniotavalbN  41030  cdlemb3  41052  cdlemg6c  41066  cdlemg6  41069  cdlemg7N  41072  cdlemg8c  41075  cdlemg8  41077  cdlemg11a  41083  cdlemg11b  41088  cdlemg12e  41093  cdlemg15a  41101  cdlemg15  41102  cdlemg16  41103  cdlemg16z  41105  cdlemg16zz  41106  cdlemg17dN  41109  cdlemg18a  41124  cdlemg20  41131  cdlemg22  41133  cdlemg24  41134  cdlemg37  41135  cdlemg31d  41146  cdlemg29  41151  cdlemg33b  41153  cdlemg33  41157  cdlemg38  41161  cdlemg39  41162  cdlemg40  41163  trlco  41173  trlcone  41174  cdlemg42  41175  cdlemg44b  41178  ltrncom  41184  trljco  41186  tendococl  41218  tendoplcl  41227  tendoplcom  41228  cdlemj2  41268  cdlemj3  41269  tendoid0  41271  tendoconid  41275  tendotr  41276  cdlemk25-3  41350  cdlemk26b-3  41351  cdlemk34  41356  cdlemk36  41359  cdlemk38  41361  cdlemkid4  41380  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk19x  41389  cdlemk53  41403  cdlemk55  41407  cdlemk55u  41412  cdlemk39u  41414  cdlemk19u  41416  cdlemk56  41417  tendoex  41421  cdleml3N  41424  cdleml5N  41426  tendospcanN  41469  cdlemm10N  41564  cdlemn11pre  41656  dihord2pre  41671  dihvalcqpre  41681  dihopelvalcpre  41694  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dihord  41710  dihmeetlem1N  41736  dihglblem5apreN  41737  dihglblem3N  41741  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetbN  41749  dihmeetlem4preN  41752  dihmeetlem5  41754  dihmeetlem7N  41756  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem12N  41764  dihmeetlem13N  41765  dihmeetlem15N  41767  dihmeetlem16N  41768  dihmeetlem17N  41769  dihmeetlem18N  41770  dihmeetlem19N  41771  dihmeetALTN  41773  dih1dimatlem0  41774  dihlspsnssN  41778  dihlspsnat  41779  mapdh8ad  42225  hdmap14lem14  42327  hgmapvvlem3  42371  aks6d1c6isolem1  42613  dvdsexpnn  42765  resubcan2  42820  mzprename  43181  eldioph2lem1  43192  lzunuz  43200  rencldnfi  43249  pellexlem2  43258  infmrgelbi  43306  pellfundglb  43313  pellfund14gap  43315  qirropth  43336  rmxycomplete  43345  congadd  43394  acongeq  43411  jm2.19  43421  jm2.23  43424  jm2.20nn  43425  jm2.27  43436  jm3.1  43448  aomclem6  43487  lnmepi  43513  lmhmfgsplit  43514  lmhmlnmsplit  43515  pwssplit4  43517  hbtlem2  43552  hbtlem5  43556  dgraa0p  43577  proot1hash  43623  iocunico  43639  oasubex  43714  oege1  43734  relexpxpmin  44144  brtrclfv2  44154  ntrclsiso  44494  ntrclskb  44496  ntrclsk3  44497  k0004lem3  44576  grur1cld  44659  ismnu  44688  grumnudlem  44712  suprnmpt  45604  wessf1ornlem  45615  projf1o  45626  snunioo1  45942  iccintsng  45953  lptre2pt  46068  limcleqr  46072  fnlimfvre  46102  limsupgtlem  46205  volioc  46400  iblspltprt  46401  stoweidlem19  46447  stoweidlem20  46448  stoweidlem22  46450  stoweidlem28  46456  stoweidlem34  46462  stoweidlem44  46472  stoweidlem60  46488  wallispilem3  46495  fourierdlem41  46576  fourierdlem42  46577  fourierdlem49  46583  fourierdlem51  46585  fourierdlem54  46588  fourierdlem74  46608  fourierdlem97  46631  caratheodorylem2  46955  ovnsubaddlem2  46999  hspmbllem2  47055  smflimmpt  47238  smflimsupmpt  47257  smfliminfmpt  47260  funfocofob  47526  fzopredsuc  47772  nnmul2b  47779  imasetpreimafvbijlemfv  47862  iccpartigtl  47883  lighneal  48074  oexpnegALTV  48153  oexpnegnz  48154  tgblthelfgott  48291  clnbgrgrim  48410  uhgrimgrlim  48463  gpgusgralem  48532  lidldomn1  48707  ofaddmndmap  48819  lincdifsn  48900  lincellss  48902  lincresunit3lem3  48950  islindeps2  48959  lindssnlvec  48962  fdivmptf  49017  refdivmptf  49018  rrx2linest  49218  itsclc0yqsollem1  49238  itsclc0b  49248  itsclquadb  49252  itscnhlinecirc02plem3  49260  diag1  49779  setc1onsubc  50077