Theorem simpl1 1187

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl11  1244  simpl21  1247  simpl31  1250  simp1l1  1262  simp2l1  1268  simp3l1  1274  3anandirs  1468  rspc3ev  3637  2nreu  4393  f1prex  7040  cocan1  7047  weniso  7107  smogt  8004  smorndom  8005  omeulem1  8208  nnmord  8258  nnmword  8259  difsnen  8599  enfixsn  8626  mapunen  8686  ac6sfi  8762  fipreima  8830  elfiun  8894  ordiso2  8979  wemaplem2  9011  wemapso  9015  en2eqpr  9433  indcardi  9467  fodomfi2  9486  iunfictbso  9540  infmap2  9640  cofsmo  9691  cfsmolem  9692  coftr  9695  fin23lem11  9739  fincssdom  9745  fin23lem26  9747  isf32lem9  9783  ac6num  9901  gchdomtri  10051  gchpwdom  10092  winainflem  10115  tskuni  10205  gruima  10224  gruf  10233  grudomon  10239  elnpi  10410  distrlem4pr  10448  prlem934  10455  addcan  10824  addcan2  10825  divmulass  11321  divmulasscom  11322  ltmul1a  11489  suprleub  11607  supmul1  11610  suprzcl  12063  uzsupss  12341  xleadd1a  12647  xlesubadd  12657  xmulasslem3  12680  xlemul2a  12683  xadddilem  12688  xadddi2  12691  ixxun  12755  icoshftf1o  12861  ioounsn  12864  snunioc  12867  lincmb01cmp  12882  iccf1o  12883  nn0p1elfzo  13081  fzofzim  13085  ltexp2a  13531  leexp2  13536  ltexp2r  13538  exple1  13541  expnlbnd2  13596  fun2dmnop0  13853  ccatass  13942  ccat2s1fvwOLD  13999  swrdswrdlem  14066  ccatopth  14078  repswpfx  14147  2cshw  14175  cshimadifsn  14191  cshimadifsn0  14192  cshco  14198  repsco  14202  s2f1o  14278  limsupgre  14838  addcn2  14950  mulcn2  14952  ntrivcvgmul  15258  binomrisefac  15396  dvdsmodexp  15615  dvdsadd2b  15656  dvdsmod  15678  oexpneg  15694  sadass  15820  gcdass  15895  rplpwr  15907  rppwr  15908  lcmfunsnlem1  15981  coprmdvds2  15998  rpmulgcd2  16000  qredeq  16001  rpdvds  16004  cncongr2  16012  rpexp  16064  prmdiveq  16123  hashgcdlem  16125  odzdvds  16132  modprmn0modprm0  16144  coprimeprodsq2  16146  pythagtriplem3  16155  pcdvdsb  16205  pcgcd1  16213  qexpz  16237  pockthg  16242  vdwnnlem1  16331  0ram  16356  ramz2  16360  lubss  17731  lubun  17733  clatleglb  17736  clatglbss  17737  mrelatglb  17794  isnsgrp  17905  issubmnd  17938  ress0g  17939  gsumccatOLD  18005  gsumccat  18006  frmdss2  18028  submefmnd  18060  mulgneg  18246  mulgdirlem  18258  submmulg  18271  subgmulg  18293  nmzsubg  18317  ghmmulg  18370  gsmsymgreqlem1  18558  pmtrfb  18593  psgnunilem4  18625  odmodnn0  18668  odnncl  18673  odmod  18674  odmulgid  18681  odmulgeq  18684  odf1o1  18697  odf1o2  18698  odngen  18702  gexdvdsi  18708  pgpfi1  18720  odcau  18729  subgslw  18741  fislw  18750  lsmssv  18768  lsmless1x  18769  lsmless2x  18770  lsmsubm  18778  lsmmod  18801  lsmmod2  18802  efgred  18874  cntzcmn  18960  ghmplusg  18966  odadd1  18968  odadd2  18969  odadd  18970  lsmcomx  18976  gsumconst  19054  ablsimpgprmd  19237  srg1zr  19279  ring1eq0  19340  mulgass2  19351  isabvd  19591  rmodislmodlem  19701  rmodislmod  19702  lssintcl  19736  0lmhm  19812  lmhmvsca  19817  reslmhm2b  19826  pwssplit1  19831  pwssplit3  19833  lspfixed  19900  lspsnat  19917  lidldvgen  20028  issubassa  20098  evlsval2  20300  psrplusgpropd  20404  coe1subfv  20434  coe1mul2  20437  xrsdsreclblem  20591  regsumsupp  20766  obselocv  20872  uvcresum  20937  frlmsslsp  20940  frlmup4  20945  lindff1  20964  f1lindf  20966  lsslindf  20974  islindf4  20982  lbslcic  20985  mhmvlin  21008  mpomatmul  21055  mamutpos  21067  scmatscmide  21116  mavmulsolcl  21160  marrepcl  21173  mdetdiag  21208  mdetunilem1  21221  mdetunilem3  21223  mdetunilem7  21227  mdetunilem9  21229  mdetmul  21232  slesolinvbi  21290  m2pmfzmap  21355  pmatcollpwlem  21388  pmatcollpw  21389  mp2pm2mplem4  21417  chpdmatlem3  21448  chfacfisfcpmat  21463  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmidpmatlem2  21479  cpmadugsumlemB  21482  cpmadugsumlemC  21483  cpmadugsumlemF  21484  riinopn  21516  neiint  21712  topssnei  21732  restntr  21790  iscnp4  21871  cnconst2  21891  cnrest2  21894  cnprest2  21898  cnpdis  21901  cnt0  21954  cnt1  21958  cnhaus  21962  ordthauslem  21991  cncmp  22000  fiuncmp  22012  sscmp  22013  hauscmp  22015  cnconn  22030  unconn  22037  nlly2i  22084  llynlly  22085  nllyidm  22097  finlocfin  22128  ptrescn  22247  xkococnlem  22267  qtopss  22323  kqfvima  22338  r0cld  22346  ordthmeolem  22409  fbssint  22446  fmf  22553  fmss  22554  elfm  22555  rnelfmlem  22560  rnelfm  22561  fmco  22569  flimss2  22580  flimss1  22581  flimrest  22591  flftg  22604  cnpflf2  22608  cnpflf  22609  flfcnp  22612  supnfcls  22628  fclsss1  22630  fclsss2  22631  fcfnei  22643  fcfelbas  22644  cnpfcfi  22648  subgntr  22715  opnsubg  22716  cldsubg  22719  ghmcnp  22723  utop2nei  22859  neipcfilu  22905  bldisj  23008  blgt0  23009  bl2in  23010  blss2ps  23013  blss2  23014  blssps  23034  blss  23035  xmetresbl  23047  lpbl  23113  blcld  23115  stdbdbl  23127  metcnp3  23150  metcnp2  23152  txmetcnp  23157  blval2  23172  nmoix  23338  nmoeq0  23345  icoopnst  23543  iocopnst  23544  xrhmeo  23550  nmhmcn  23724  cphsqrtcl2  23790  cphsqrtcl3  23791  cfil3i  23872  caublcls  23912  bcthlem5  23931  cmetcusp1  23956  cssbn  23978  rrxcph  23995  pjth  24042  ovoliunlem2  24104  volun  24146  volsup2  24206  mbfimaopn2  24258  iblconst  24418  itgconst  24419  dvcnp2  24517  dvcn  24518  deg1mul3le  24710  deg1tmle  24711  dvdsq1p  24754  ig1peu  24765  ig1pdvds  24770  coeid3  24830  dgrmulc  24861  efcvx  25037  tanord  25122  logdivlti  25203  logccv  25246  recxpcl  25258  cxpeq  25338  ang180  25392  isosctrlem2  25397  cxp2lim  25554  amgm  25568  muval1  25710  dvdssqf  25715  mumullem2  25757  mumul  25758  bcmono  25853  lgsfcl2  25879  lgsdilem  25900  lgsdirprm  25907  lgsdir  25908  lgsdi  25910  lgsne0  25911  padicabv  26206  brbtwn2  26691  colinearalglem1  26692  colinearalg  26696  axcgrtr  26701  axsegconlem8  26710  axsegconlem9  26711  axsegconlem10  26712  axcontlem8  26757  axcontlem10  26759  elntg2  26771  vtxdlfuhgr1v  27261  umgr2wlk  27728  erclwwlksym  27799  clwwlkfo  27829  clwwlkext2edg  27835  erclwwlknsym  27849  clwwlknon1  27876  numclwwlk2lem1  28155  numclwwlk5  28167  frgrregord13  28175  nvmul0or  28427  ipval2lem2  28481  lnomul  28537  shless  29136  shlej1  29137  pjspansn  29354  hoadddi  29580  kbmul  29732  homco2  29754  kbass2  29894  eliccelico  30500  elicoelioo  30501  iocinioc2  30502  iocinif  30504  swrdrn2  30628  xrge0adddir  30679  xrge0npcan  30681  archiabl  30827  ress1r  30860  rhmdvdsr  30891  ssmxidl  30979  pstmfval  31136  fmcncfil  31174  zrhnm  31210  qqhnm  31231  measvunilem  31471  volfiniune  31489  dya2iocnrect  31539  sibfinima  31597  probun  31677  probinc  31679  cndprob01  31693  signstfvp  31841  bnj517  32157  bnj594  32184  pconnpi1  32484  cvmsss2  32521  mrsubcv  32757  msubvrs  32807  dvdspw  32982  br6  32993  br4  32994  frpomin  33078  frrlem4  33126  frrlem10  33132  fprlem1  33137  nosep1o  33186  nosepssdm  33190  nolt02olem  33198  nosupres  33207  nosupbnd1lem1  33208  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  nosupbnd2  33216  noetalem2  33218  cgrcomim  33450  cgrtriv  33463  cgrextend  33469  segconeq  33471  btwntriv2  33473  btwnintr  33480  btwnexch3  33481  btwnouttr2  33483  trisegint  33489  cgrsub  33506  cgrxfr  33516  btwnxfr  33517  lineext  33537  btwnconn1lem13  33560  btwnconn1lem14  33561  btwnconn3  33564  segcon2  33566  brsegle  33569  brsegle2  33570  segletr  33575  segleantisym  33576  seglelin  33577  outsideofeu  33592  lineunray  33608  lineelsb2  33609  ivthALT  33683  lindsenlbs  34902  areacirc  35002  cocanfo  35008  upixp  35019  ismtyima  35096  rrndstprj2  35124  zerdivemp1x  35240  lsatfixedN  36160  lssat  36167  eqlkr  36250  eqlkr2  36251  lkrlsp  36253  lshpkrlem4  36264  opposet  36332  cvrcon3b  36428  cvrcmp  36434  atlen0  36461  atnle  36468  atlatmstc  36470  cvlatexch3  36489  cvlsupr2  36494  hlsupr2  36538  hlrelat2  36554  cvrexchlem  36570  lnnat  36578  atcvrj2b  36583  atle  36587  atexchcvrN  36591  atbtwn  36597  athgt  36607  3dimlem3  36612  3dim1  36618  1cvratlt  36625  1cvrjat  36626  ps-1  36628  ps-2  36629  3atlem3  36636  3atlem5  36638  3atlem7  36640  llni  36659  llni2  36663  atcvrlln2  36670  llnexatN  36672  llncmp  36673  2llnmat  36675  2at0mat0  36676  lplni  36683  lplnnle2at  36692  2atnelpln  36695  lplnllnneN  36707  llncvrlpln2  36708  2lplnmN  36710  2llnmj  36711  lplncmp  36713  lplnexatN  36714  lplnexllnN  36715  2llnm3N  36720  lvoli  36726  lvoli3  36728  islvol2aN  36743  4atlem0a  36744  4atlem3  36747  4atlem3a  36748  4atlem4a  36750  4atlem4b  36751  4atlem4c  36752  4atlem4d  36753  4atlem10b  36756  4atlem11  36760  4atlem12  36763  lplncvrlvol2  36766  lvolcmp  36768  2lplnmj  36773  islinei  36891  pmapglbx  36920  linepmap  36926  lneq2at  36929  lnjatN  36931  lncvrat  36933  lncmp  36934  2llnma3r  36939  elpaddatriN  36954  elpaddat  36955  paddcom  36964  paddss1  36968  paddss2  36969  paddss12  36970  paddasslem6  36976  paddasslem7  36977  paddasslem8  36978  paddasslem9  36979  paddasslem15  36985  pmodlem2  36998  pmodl42N  37002  pmapjoin  37003  llnmod1i2  37011  2polcon4bN  37069  polcon2bN  37071  poml4N  37104  poml6N  37106  osumcllem1N  37107  osumcllem2N  37108  osumcllem11N  37117  osumclN  37118  pmapojoinN  37119  pexmidlem2N  37122  pexmidlem3N  37123  pexmidlem4N  37124  pexmidlem6N  37126  pexmidlem7N  37127  pl42lem2N  37131  pl42lem3N  37132  pl42lem4N  37133  pl42N  37134  lhpexle2lem  37160  lhpexle3lem  37162  lhpexle3  37163  lhpmcvr3  37176  lhp2at0nle  37186  lhprelat3N  37191  4atex  37227  4atex2  37228  lauteq  37246  lautco  37248  ltrncoidN  37279  ltrneq2  37299  ltrnnidn  37325  ltrnideq  37326  trlnid  37330  ltrnatlw  37334  trlnle  37337  trlval3  37338  trlval4  37339  cdlemc  37348  cdlemd5  37353  cdlemd9  37357  ltrneq3  37359  cdleme0moN  37376  cdleme20  37475  cdleme21j  37487  cdleme21  37488  cdleme27cl  37517  cdlemefrs29bpre0  37547  cdlemefs27cl  37564  cdlemefs32sn1aw  37565  cdleme43fsv1snlem  37571  cdleme32d  37595  cdleme32f  37597  cdleme32le  37598  cdleme35h2  37608  cdleme38n  37615  cdleme40m  37618  cdleme41snaw  37627  cdleme42ke  37636  cdleme17d3  37647  cdleme48fvg  37651  cdlemeg46fvcl  37657  cdlemeg46fgN  37685  cdleme48gfv1  37687  cdleme48fgv  37689  cdleme50trn3  37704  trlord  37720  ltrniotavalbN  37735  cdlemb3  37757  cdlemg6c  37771  cdlemg6  37774  cdlemg7N  37777  cdlemg8c  37780  cdlemg8  37782  cdlemg11a  37788  cdlemg11b  37793  cdlemg12e  37798  cdlemg15a  37806  cdlemg15  37807  cdlemg16  37808  cdlemg16z  37810  cdlemg16zz  37811  cdlemg17dN  37814  cdlemg18a  37829  cdlemg20  37836  cdlemg22  37838  cdlemg24  37839  cdlemg37  37840  cdlemg31d  37851  cdlemg29  37856  cdlemg33b  37858  cdlemg33  37862  cdlemg38  37866  cdlemg39  37867  cdlemg40  37868  trlco  37878  trlcone  37879  cdlemg42  37880  cdlemg44b  37883  ltrncom  37889  trljco  37891  tendococl  37923  tendoplcl  37932  tendoplcom  37933  cdlemj2  37973  cdlemj3  37974  tendoid0  37976  tendoconid  37980  tendotr  37981  cdlemk25-3  38055  cdlemk26b-3  38056  cdlemk34  38061  cdlemk36  38064  cdlemk38  38066  cdlemkid4  38085  cdlemk35s-id  38089  cdlemk39s-id  38091  cdlemk19x  38094  cdlemk53  38108  cdlemk55  38112  cdlemk55u  38117  cdlemk39u  38119  cdlemk19u  38121  cdlemk56  38122  tendoex  38126  cdleml3N  38129  cdleml5N  38131  tendospcanN  38174  cdlemm10N  38269  cdlemn11pre  38361  dihord2pre  38376  dihvalcqpre  38386  dihopelvalcpre  38399  dihord6apre  38407  dihord5b  38410  dihord5apre  38413  dihord  38415  dihmeetlem1N  38441  dihglblem5apreN  38442  dihglblem3N  38446  dihmeetlem2N  38450  dihglbcpreN  38451  dihmeetbN  38454  dihmeetlem4preN  38457  dihmeetlem5  38459  dihmeetlem7N  38461  dihmeetlem10N  38467  dihmeetlem11N  38468  dihmeetlem12N  38469  dihmeetlem13N  38470  dihmeetlem15N  38472  dihmeetlem16N  38473  dihmeetlem17N  38474  dihmeetlem18N  38475  dihmeetlem19N  38476  dihmeetALTN  38478  dih1dimatlem0  38479  dihlspsnssN  38483  dihlspsnat  38484  mapdh8ad  38930  hdmap14lem14  39032  hgmapvvlem3  39076  resubcan2  39267  mzprename  39395  eldioph2lem1  39406  lzunuz  39414  rencldnfi  39467  pellexlem2  39476  infmrgelbi  39524  pellfundglb  39531  pellfund14gap  39533  qirropth  39554  rmxycomplete  39563  congadd  39612  acongeq  39629  jm2.19  39639  jm2.23  39642  jm2.20nn  39643  jm2.27  39654  jm3.1  39666  aomclem6  39708  lnmepi  39734  lmhmfgsplit  39735  lmhmlnmsplit  39736  pwssplit4  39738  hbtlem2  39773  hbtlem5  39777  dgraa0p  39798  proot1hash  39849  iocunico  39866  relexpxpmin  40111  brtrclfv2  40121  ntrclsiso  40466  ntrclskb  40468  ntrclsk3  40469  k0004lem3  40548  grur1cld  40617  ismnu  40646  grumnudlem  40670  suprnmpt  41479  wessf1ornlem  41494  projf1o  41508  snunioo1  41837  iccintsng  41848  lptre2pt  41970  limcleqr  41974  fnlimfvre  42004  limsupgtlem  42107  volioc  42306  iblspltprt  42307  stoweidlem19  42353  stoweidlem20  42354  stoweidlem22  42356  stoweidlem28  42362  stoweidlem34  42368  stoweidlem44  42378  stoweidlem60  42394  wallispilem3  42401  fourierdlem41  42482  fourierdlem42  42483  fourierdlem49  42489  fourierdlem51  42491  fourierdlem54  42494  fourierdlem74  42514  fourierdlem97  42537  caratheodorylem2  42858  ovnsubaddlem2  42902  hspmbllem2  42958  smflimmpt  43133  smflimsupmpt  43152  smfliminfmpt  43155  fzopredsuc  43572  fzoopth  43576  imasetpreimafvbijlemfv  43611  iccpartigtl  43632  lighneal  43825  oexpnegALTV  43891  oexpnegnz  43892  tgblthelfgott  44029  lidldomn1  44241  ofaddmndmap  44441  lincdifsn  44528  lincellss  44530  lincresunit3lem3  44578  islindeps2  44587  lindssnlvec  44590  fdivmptf  44650  refdivmptf  44651  rrx2linest  44778  itsclc0yqsollem1  44798  itsclc0b  44808  itsclquadb  44812  itscnhlinecirc02plem3  44820