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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  simpl11  1267  simpl21  1270  simpl31  1273  simp1l1  1285  simp2l1  1291  simp3l1  1297  3anandirs  1501  rspc3ev  3599  2nreu  4410  predtrss  6325  frpomin  6343  f1prex  7284  cocan1  7291  weniso  7354  frrlem4  8287  frrlem10  8293  fprlem1  8298  smogt  8355  smocdmdom  8356  omeulem1  8568  nnmord  8619  nnmword  8620  naddasslem1  8682  naddasslem2  8683  difsnen  9048  enfixsn  9075  mapunen  9135  ac6sfi  9245  fipreima  9316  elfiun  9391  ordiso2  9478  wemaplem2  9510  en2eqpr  9992  indcardi  10026  fodomfi2  10045  iunfictbso  10099  infmap2  10201  cofsmo  10254  cfsmolem  10255  coftr  10258  fin23lem11  10302  fincssdom  10308  fin23lem26  10310  isf32lem9  10346  ac6num  10464  gchdomtri  10615  gchpwdom  10656  winainflem  10679  tskuni  10769  gruima  10788  gruf  10797  grudomon  10803  elnpi  10974  distrlem4pr  11012  prlem934  11019  addcan  11395  addcan2  11396  divmulass  11896  divmulasscom  11897  ltmul1a  12065  suprleub  12182  supmul1  12185  suprzcl  12677  uzsupss  12965  xleadd1a  13280  xlesubadd  13290  xmulasslem3  13313  xlemul2a  13316  xadddilem  13321  xadddi2  13324  ixxun  13389  icoshftf1o  13502  ioounsn  13505  snunioc  13508  lincmb01cmp  13523  iccf1o  13524  nn0p1elfzo  13733  fzofzim  13740  fzoopth  13793  ltexp2a  14204  leexp2  14209  ltexp2r  14211  exple1  14215  expnlbnd2  14272  fun2dmnop0  14543  ccatass  14628  swrdswrdlem  14743  ccatopth  14755  repswpfx  14824  2cshw  14852  cshimadifsn  14868  cshimadifsn0  14869  cshco  14875  repsco  14879  s2f1o  14955  limsupgre  15534  addcn2  15647  mulcn2  15649  ntrivcvgmul  15958  binomrisefac  16097  dvdsmodexp  16319  dvdsadd2b  16365  dvdsexp2im  16386  dvdsmod  16388  oexpneg  16404  sadass  16530  gcdass  16606  rplpwr  16617  lcmfunsnlem1  16696  coprmdvds2  16713  rpmulgcd2  16715  qredeq  16716  rpdvds  16719  cncongr2  16727  rpexp  16782  prmdiveq  16846  hashgcdlem  16848  odzdvds  16856  modprmn0modprm0  16868  coprimeprodsq2  16870  pythagtriplem3  16879  pcdvdsb  16930  pcgcd1  16938  qexpz  16962  pockthg  16967  vdwnnlem1  17056  0ram  17081  ramz2  17085  lubss  18570  lubun  18572  clatleglb  18575  clatglbss  18576  mrelatglb  18617  isnsgrp  18782  issubmnd  18820  ress0g  18821  mhmvlin  18860  gsumccat  18901  frmdss2  18923  submefmnd  18955  mulgneg  19159  mulgdirlem  19172  submmulg  19185  subgmulg  19208  nmzsubg  19232  ghmmulg  19299  gsmsymgreqlem1  19501  pmtrfb  19536  psgnunilem4  19568  odmodnn0  19611  odnncl  19616  odmod  19617  odmulgid  19625  odmulgeq  19628  odf1o1  19643  odf1o2  19644  odngen  19648  gexdvdsi  19654  pgpfi1  19666  odcau  19675  subgslw  19687  fislw  19696  lsmssv  19714  lsmless1x  19715  lsmless2x  19716  lsmsubm  19724  lsmmod  19746  lsmmod2  19747  efgred  19819  cntzcmn  19911  ghmplusg  19917  odadd1  19919  odadd2  19920  odadd  19921  lsmcomx  19927  gsumconst  20005  ablsimpgprmd  20188  ring1eq0  20382  mulgass2  20393  rngisom1  20549  rhmdvdsr  20592  isabvd  20896  rmodislmodlem  21031  rmodislmod  21032  lssintcl  21066  0lmhm  21142  lmhmvsca  21147  reslmhm2b  21156  pwssplit1  21161  pwssplit3  21163  lspfixed  21233  lspsnat  21250  unichnlidl  21343  pidlnz  21355  rnglidlrng  21362  2idlcpblrng  21391  lidldvgen  21483  xrsdsreclblem  21544  regsumsupp  21753  obselocv  21859  uvcresum  21924  frlmsslsp  21927  frlmup4  21932  lindff1  21951  f1lindf  21953  lsslindf  21961  islindf4  21969  lbslcic  21972  issubassa  21998  evlsval2  22219  psrplusgpropd  22376  coe1subfv  22408  coe1mul2  22411  mpomatmul  22584  mamutpos  22596  scmatscmide  22645  mavmulsolcl  22689  marrepcl  22702  mdetdiag  22737  mdetunilem1  22750  mdetunilem3  22752  mdetunilem7  22756  mdetunilem9  22758  mdetmul  22761  slesolinvbi  22819  m2pmfzmap  22885  pmatcollpwlem  22918  pmatcollpw  22919  mp2pm2mplem4  22947  chpdmatlem3  22978  chfacfisfcpmat  22993  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  chfacfpmmulgsum2  23003  cayhamlem1  23004  cpmidpmatlem2  23009  cpmadugsumlemB  23012  cpmadugsumlemC  23013  cpmadugsumlemF  23014  riinopn  23046  neiint  23242  topssnei  23262  restntr  23320  iscnp4  23401  cnconst2  23421  cnrest2  23424  cnprest2  23428  cnpdis  23431  cnt0  23484  cnt1  23488  cnhaus  23492  ordthauslem  23521  cncmp  23530  fiuncmp  23542  sscmp  23543  hauscmp  23545  cnconn  23560  unconn  23567  nlly2i  23614  llynlly  23615  nllyidm  23627  finlocfin  23658  ptrescn  23777  xkococnlem  23797  qtopss  23853  kqfvima  23868  r0cld  23876  ordthmeolem  23939  fbssint  23976  fmf  24083  fmss  24084  elfm  24085  rnelfmlem  24090  rnelfm  24091  fmco  24099  flimss2  24110  flimss1  24111  flimrest  24121  flftg  24134  cnpflf2  24138  cnpflf  24139  flfcnp  24142  supnfcls  24158  fclsss1  24160  fclsss2  24161  fcfnei  24173  fcfelbas  24174  cnpfcfi  24178  subgntr  24245  opnsubg  24246  cldsubg  24249  ghmcnp  24253  utop2nei  24388  neipcfilu  24433  bldisj  24536  blgt0  24537  bl2in  24538  blss2ps  24541  blss2  24542  blssps  24562  blss  24563  xmetresbl  24575  lpbl  24641  blcld  24643  stdbdbl  24655  metcnp3  24678  metcnp2  24680  txmetcnp  24685  blval2  24700  nmoix  24867  nmoeq0  24874  icoopnst  25079  iocopnst  25080  xrhmeo  25086  nmhmcn  25260  cphsqrtcl2  25326  cphsqrtcl3  25327  cfil3i  25409  caublcls  25449  bcthlem5  25468  cmetcusp1  25493  cssbn  25515  rrxcph  25532  pjth  25579  ovoliunlem2  25643  volun  25685  volsup2  25745  mbfimaopn2  25797  iblconst  25958  itgconst  25959  dvcnp2  26060  dvcn  26061  deg1mul3le  26255  deg1tmle  26256  dvdsq1p  26301  ig1peu  26313  ig1pdvds  26318  coeid3  26378  dgrmulc  26409  efcvx  26593  tanord  26684  logdivlti  26766  logccv  26809  recxpcl  26821  cxpeq  26903  ang180  26960  isosctrlem2  26965  cxp2lim  27122  amgm  27136  muval1  27278  dvdssqf  27283  mumullem2  27325  mumul  27326  bcmono  27422  lgsfcl2  27448  lgsdilem  27469  lgsdirprm  27476  lgsdir  27477  lgsdi  27479  lgsne0  27480  padicabv  27775  nosep1o  27826  nosep2o  27827  nosepssdm  27831  nolt02olem  27839  nosupres  27852  nosupbnd1lem1  27853  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd1lem6  27858  nosupbnd2  27861  noinfres  27867  noinfbnd1lem1  27868  noinfbnd1lem4  27871  noinfbnd1lem6  27873  noinfbnd2  27876  noetasuplem3  27880  noetalem1  27886  cutbdaybnd  27969  ltslpss  28082  leslss  28083  coinitslts  28093  addsass  28179  addsdi  28329  mulsass  28340  norecdiv  28364  bdayfinbndlem1  28641  z12bdaylem  28658  brbtwn2  29236  colinearalglem1  29237  colinearalg  29241  axcgrtr  29246  axsegconlem8  29255  axsegconlem9  29256  axsegconlem10  29257  axcontlem8  29302  axcontlem10  29304  elntg2  29316  vtxdlfuhgr1v  29810  umgr2wlk  30279  erclwwlksym  30353  clwwlkfo  30382  clwwlkext2edg  30388  erclwwlknsym  30402  clwwlknon1  30429  numclwwlk2lem1  30708  numclwwlk5  30720  frgrregord13  30728  nvmul0or  30983  ipval2lem2  31037  lnomul  31093  shless  31692  shlej1  31693  pjspansn  31910  hoadddi  32136  kbmul  32288  homco2  32310  kbass2  32450  eliccelico  33103  elicoelioo  33104  iocinioc2  33105  iocinif  33107  swrdrn2  33255  xrge0adddir  33319  xrge0npcan  33321  archiabl  33499  ress1r  33533  grplsm0l  33693  intlidl  33709  ssmxidl  33738  pstmfval  34267  fmcncfil  34302  zrhnm  34338  qqhnm  34361  measvunilem  34583  volfiniune  34601  dya2iocnrect  34652  sibfinima  34710  probun  34790  probinc  34792  cndprob01  34806  signstfvp  34939  bnj517  35254  bnj594  35281  fissorduni  35461  pconnpi1  35710  cvmsss2  35747  mrsubcv  35983  msubvrs  36033  br6  36230  br4  36231  cgrcomim  36462  cgrtriv  36475  cgrextend  36481  segconeq  36483  btwntriv2  36485  btwnintr  36492  btwnexch3  36493  btwnouttr2  36495  trisegint  36501  cgrsub  36518  cgrxfr  36528  btwnxfr  36529  lineext  36549  btwnconn1lem13  36572  btwnconn1lem14  36573  btwnconn3  36576  segcon2  36578  brsegle  36581  brsegle2  36582  segletr  36587  segleantisym  36588  seglelin  36589  outsideofeu  36604  lineunray  36620  lineelsb2  36621  nmulss1  36672  ltnmul  36674  nmulle  36675  ltnadd  36676  naddle  36677  ivthALT  36827  weiunpo  36957  weiunso  36958  weiunfr  36959  weiunse  36960  lindsenlbs  38247  areacirc  38345  cocanfo  38351  upixp  38361  ismtyima  38435  rrndstprj2  38463  zerdivemp1x  38579  lsatfixedN  39764  lssat  39771  eqlkr  39854  eqlkr2  39855  lkrlsp  39857  lshpkrlem4  39868  opposet  39936  cvrcon3b  40032  cvrcmp  40038  atlen0  40065  atnle  40072  atlatmstc  40074  cvlatexch3  40093  cvlsupr2  40098  hlsupr2  40142  hlrelat2  40158  cvrexchlem  40174  lnnat  40182  atcvrj2b  40187  atle  40191  atexchcvrN  40195  atbtwn  40201  athgt  40211  3dimlem3  40216  3dim1  40222  1cvratlt  40229  1cvrjat  40230  ps-1  40232  ps-2  40233  3atlem3  40240  3atlem5  40242  3atlem7  40244  llni  40263  llni2  40267  atcvrlln2  40274  llnexatN  40276  llncmp  40277  2llnmat  40279  2at0mat0  40280  lplni  40287  lplnnle2at  40296  2atnelpln  40299  lplnllnneN  40311  llncvrlpln2  40312  2lplnmN  40314  2llnmj  40315  lplncmp  40317  lplnexatN  40318  lplnexllnN  40319  2llnm3N  40324  lvoli  40330  lvoli3  40332  islvol2aN  40347  4atlem0a  40348  4atlem3  40351  4atlem3a  40352  4atlem4a  40354  4atlem4b  40355  4atlem4c  40356  4atlem4d  40357  4atlem10b  40360  4atlem11  40364  4atlem12  40367  lplncvrlvol2  40370  lvolcmp  40372  2lplnmj  40377  islinei  40495  pmapglbx  40524  linepmap  40530  lneq2at  40533  lnjatN  40535  lncvrat  40537  lncmp  40538  2llnma3r  40543  elpaddatriN  40558  elpaddat  40559  paddcom  40568  paddss1  40572  paddss2  40573  paddss12  40574  paddasslem6  40580  paddasslem7  40581  paddasslem8  40582  paddasslem9  40583  paddasslem15  40589  pmodlem2  40602  pmodl42N  40606  pmapjoin  40607  llnmod1i2  40615  2polcon4bN  40673  polcon2bN  40675  poml4N  40708  poml6N  40710  osumcllem1N  40711  osumcllem2N  40712  osumcllem11N  40721  osumclN  40722  pmapojoinN  40723  pexmidlem2N  40726  pexmidlem3N  40727  pexmidlem4N  40728  pexmidlem6N  40730  pexmidlem7N  40731  pl42lem2N  40735  pl42lem3N  40736  pl42lem4N  40737  pl42N  40738  lhpexle2lem  40764  lhpexle3lem  40766  lhpexle3  40767  lhpmcvr3  40780  lhp2at0nle  40790  lhprelat3N  40795  4atex  40831  4atex2  40832  lauteq  40850  lautco  40852  ltrncoidN  40883  ltrneq2  40903  ltrnnidn  40929  ltrnideq  40930  trlnid  40934  ltrnatlw  40938  trlnle  40941  trlval3  40942  trlval4  40943  cdlemc  40952  cdlemd5  40957  cdlemd9  40961  ltrneq3  40963  cdleme0moN  40980  cdleme20  41079  cdleme21j  41091  cdleme21  41092  cdleme27cl  41121  cdlemefrs29bpre0  41151  cdlemefs27cl  41168  cdlemefs32sn1aw  41169  cdleme43fsv1snlem  41175  cdleme32d  41199  cdleme32f  41201  cdleme32le  41202  cdleme35h2  41212  cdleme38n  41219  cdleme40m  41222  cdleme41snaw  41231  cdleme42ke  41240  cdleme17d3  41251  cdleme48fvg  41255  cdlemeg46fvcl  41261  cdlemeg46fgN  41289  cdleme48gfv1  41291  cdleme48fgv  41293  cdleme50trn3  41308  trlord  41324  ltrniotavalbN  41339  cdlemb3  41361  cdlemg6c  41375  cdlemg6  41378  cdlemg7N  41381  cdlemg8c  41384  cdlemg8  41386  cdlemg11a  41392  cdlemg11b  41397  cdlemg12e  41402  cdlemg15a  41410  cdlemg15  41411  cdlemg16  41412  cdlemg16z  41414  cdlemg16zz  41415  cdlemg17dN  41418  cdlemg18a  41433  cdlemg20  41440  cdlemg22  41442  cdlemg24  41443  cdlemg37  41444  cdlemg31d  41455  cdlemg29  41460  cdlemg33b  41462  cdlemg33  41466  cdlemg38  41470  cdlemg39  41471  cdlemg40  41472  trlco  41482  trlcone  41483  cdlemg42  41484  cdlemg44b  41487  ltrncom  41493  trljco  41495  tendococl  41527  tendoplcl  41536  tendoplcom  41537  cdlemj2  41577  cdlemj3  41578  tendoid0  41580  tendoconid  41584  tendotr  41585  cdlemk25-3  41659  cdlemk26b-3  41660  cdlemk34  41665  cdlemk36  41668  cdlemk38  41670  cdlemkid4  41689  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk19x  41698  cdlemk53  41712  cdlemk55  41716  cdlemk55u  41721  cdlemk39u  41723  cdlemk19u  41725  cdlemk56  41726  tendoex  41730  cdleml3N  41733  cdleml5N  41735  tendospcanN  41778  cdlemm10N  41873  cdlemn11pre  41965  dihord2pre  41980  dihvalcqpre  41990  dihopelvalcpre  42003  dihord6apre  42011  dihord5b  42014  dihord5apre  42017  dihord  42019  dihmeetlem1N  42045  dihglblem5apreN  42046  dihglblem3N  42050  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetbN  42058  dihmeetlem4preN  42061  dihmeetlem5  42063  dihmeetlem7N  42065  dihmeetlem10N  42071  dihmeetlem11N  42072  dihmeetlem12N  42073  dihmeetlem13N  42074  dihmeetlem15N  42076  dihmeetlem16N  42077  dihmeetlem17N  42078  dihmeetlem18N  42079  dihmeetlem19N  42080  dihmeetALTN  42082  dih1dimatlem0  42083  dihlspsnssN  42087  dihlspsnat  42088  mapdh8ad  42534  hdmap14lem14  42636  hgmapvvlem3  42680  aks6d1c6isolem1  42922  dvdsexpnn  43075  resubcan2  43130  mzprename  43463  eldioph2lem1  43474  lzunuz  43482  rencldnfi  43531  pellexlem2  43540  infmrgelbi  43588  pellfundglb  43595  pellfund14gap  43597  qirropth  43618  rmxycomplete  43627  congadd  43676  acongeq  43693  jm2.19  43703  jm2.23  43706  jm2.20nn  43707  jm2.27  43718  jm3.1  43730  aomclem6  43769  lnmepi  43795  lmhmfgsplit  43796  lmhmlnmsplit  43797  pwssplit4  43799  hbtlem2  43834  hbtlem5  43838  dgraa0p  43859  proot1hash  43905  iocunico  43921  oasubex  43996  oege1  44016  relexpxpmin  44426  brtrclfv2  44436  ntrclsiso  44776  ntrclskb  44778  ntrclsk3  44779  k0004lem3  44858  grur1cld  44939  ismnu  44954  grumnudlem  44978  suprnmpt  45875  wessf1ornlem  45886  projf1o  45897  snunioo1  46211  iccintsng  46222  lptre2pt  46337  limcleqr  46341  fnlimfvre  46371  limsupgtlem  46474  volioc  46669  iblspltprt  46670  stoweidlem19  46716  stoweidlem20  46717  stoweidlem22  46719  stoweidlem28  46725  stoweidlem34  46731  stoweidlem44  46741  stoweidlem60  46757  wallispilem3  46764  fourierdlem41  46845  fourierdlem42  46846  fourierdlem49  46852  fourierdlem51  46854  fourierdlem54  46857  fourierdlem74  46877  fourierdlem97  46900  caratheodorylem2  47224  ovnsubaddlem2  47268  hspmbllem2  47324  smflimmpt  47507  smflimsupmpt  47526  smfliminfmpt  47529  funfocofob  47798  fzopredsuc  48044  nnmul2b  48051  imasetpreimafvbijlemfv  48134  iccpartigtl  48155  lighneal  48346  oexpnegALTV  48425  oexpnegnz  48426  tgblthelfgott  48563  clnbgrgrim  48682  uhgrimgrlim  48735  gpgusgralem  48804  lidldomn1  48979  ofaddmndmap  49106  lincdifsn  49187  lincellss  49189  lincresunit3lem3  49237  islindeps2  49246  lindssnlvec  49249  fdivmptf  49304  refdivmptf  49305  rrx2linest  49505  itsclc0yqsollem1  49525  itsclc0b  49535  itsclquadb  49539  itscnhlinecirc02plem3  49547  diag1  50065  setc1onsubc  50363