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  3618  2nreu  4419  predtrss  6311  frpomin  6329  f1prex  7276  cocan1  7283  weniso  7346  frrlem4  8286  frrlem10  8292  fprlem1  8297  smogt  8379  smocdmdom  8380  omeulem1  8592  nnmord  8642  nnmword  8643  naddasslem1  8704  naddasslem2  8705  difsnen  9065  enfixsn  9093  mapunen  9158  ac6sfi  9290  fipreima  9368  elfiun  9440  ordiso2  9527  wemaplem2  9559  en2eqpr  10019  indcardi  10053  fodomfi2  10072  iunfictbso  10126  infmap2  10229  cofsmo  10281  cfsmolem  10282  coftr  10285  fin23lem11  10329  fincssdom  10335  fin23lem26  10337  isf32lem9  10373  ac6num  10491  gchdomtri  10641  gchpwdom  10682  winainflem  10705  tskuni  10795  gruima  10814  gruf  10823  grudomon  10829  elnpi  11000  distrlem4pr  11038  prlem934  11045  addcan  11417  addcan2  11418  divmulass  11917  divmulasscom  11918  ltmul1a  12088  suprleub  12206  supmul1  12209  suprzcl  12671  uzsupss  12954  xleadd1a  13267  xlesubadd  13277  xmulasslem3  13300  xlemul2a  13303  xadddilem  13308  xadddi2  13311  ixxun  13376  icoshftf1o  13489  ioounsn  13492  snunioc  13495  lincmb01cmp  13510  iccf1o  13511  nn0p1elfzo  13717  fzofzim  13724  fzoopth  13776  ltexp2a  14182  leexp2  14187  ltexp2r  14189  exple1  14193  expnlbnd2  14250  fun2dmnop0  14520  ccatass  14604  swrdswrdlem  14720  ccatopth  14732  repswpfx  14801  2cshw  14829  cshimadifsn  14846  cshimadifsn0  14847  cshco  14853  repsco  14857  s2f1o  14933  limsupgre  15495  addcn2  15608  mulcn2  15610  ntrivcvgmul  15916  binomrisefac  16056  dvdsmodexp  16278  dvdsadd2b  16323  dvdsexp2im  16344  dvdsmod  16346  oexpneg  16362  sadass  16488  gcdass  16564  rplpwr  16575  lcmfunsnlem1  16654  coprmdvds2  16671  rpmulgcd2  16673  qredeq  16674  rpdvds  16677  cncongr2  16685  rpexp  16739  prmdiveq  16803  hashgcdlem  16805  odzdvds  16813  modprmn0modprm0  16825  coprimeprodsq2  16827  pythagtriplem3  16836  pcdvdsb  16887  pcgcd1  16895  qexpz  16919  pockthg  16924  vdwnnlem1  17013  0ram  17038  ramz2  17042  lubss  18521  lubun  18523  clatleglb  18526  clatglbss  18527  mrelatglb  18568  isnsgrp  18699  issubmnd  18737  ress0g  18738  mhmvlin  18777  gsumccat  18817  frmdss2  18839  submefmnd  18871  mulgneg  19073  mulgdirlem  19086  submmulg  19099  subgmulg  19121  nmzsubg  19146  ghmmulg  19209  gsmsymgreqlem1  19409  pmtrfb  19444  psgnunilem4  19476  odmodnn0  19519  odnncl  19524  odmod  19525  odmulgid  19533  odmulgeq  19536  odf1o1  19551  odf1o2  19552  odngen  19556  gexdvdsi  19562  pgpfi1  19574  odcau  19583  subgslw  19595  fislw  19604  lsmssv  19622  lsmless1x  19623  lsmless2x  19624  lsmsubm  19632  lsmmod  19654  lsmmod2  19655  efgred  19727  cntzcmn  19819  ghmplusg  19825  odadd1  19827  odadd2  19828  odadd  19829  lsmcomx  19835  gsumconst  19913  ablsimpgprmd  20096  srg1zr  20173  ring1eq0  20256  mulgass2  20267  rngisom1  20424  rhmdvdsr  20466  isabvd  20770  rmodislmodlem  20884  rmodislmod  20885  lssintcl  20919  0lmhm  20996  lmhmvsca  21001  reslmhm2b  21010  pwssplit1  21015  pwssplit3  21017  lspfixed  21087  lspsnat  21104  rnglidlrng  21206  2idlcpblrng  21230  lidldvgen  21293  xrsdsreclblem  21378  regsumsupp  21580  obselocv  21686  uvcresum  21751  frlmsslsp  21754  frlmup4  21759  lindff1  21778  f1lindf  21780  lsslindf  21788  islindf4  21796  lbslcic  21799  issubassa  21825  evlsval2  22043  psrplusgpropd  22169  coe1subfv  22201  coe1mul2  22204  mpomatmul  22382  mamutpos  22394  scmatscmide  22443  mavmulsolcl  22487  marrepcl  22500  mdetdiag  22535  mdetunilem1  22548  mdetunilem3  22550  mdetunilem7  22554  mdetunilem9  22556  mdetmul  22559  slesolinvbi  22617  m2pmfzmap  22683  pmatcollpwlem  22716  pmatcollpw  22717  mp2pm2mplem4  22745  chpdmatlem3  22776  chfacfisfcpmat  22791  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  chfacfpmmulgsum2  22801  cayhamlem1  22802  cpmidpmatlem2  22807  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  riinopn  22844  neiint  23040  topssnei  23060  restntr  23118  iscnp4  23199  cnconst2  23219  cnrest2  23222  cnprest2  23226  cnpdis  23229  cnt0  23282  cnt1  23286  cnhaus  23290  ordthauslem  23319  cncmp  23328  fiuncmp  23340  sscmp  23341  hauscmp  23343  cnconn  23358  unconn  23365  nlly2i  23412  llynlly  23413  nllyidm  23425  finlocfin  23456  ptrescn  23575  xkococnlem  23595  qtopss  23651  kqfvima  23666  r0cld  23674  ordthmeolem  23737  fbssint  23774  fmf  23881  fmss  23882  elfm  23883  rnelfmlem  23888  rnelfm  23889  fmco  23897  flimss2  23908  flimss1  23909  flimrest  23919  flftg  23932  cnpflf2  23936  cnpflf  23937  flfcnp  23940  supnfcls  23956  fclsss1  23958  fclsss2  23959  fcfnei  23971  fcfelbas  23972  cnpfcfi  23976  subgntr  24043  opnsubg  24044  cldsubg  24047  ghmcnp  24051  utop2nei  24187  neipcfilu  24232  bldisj  24335  blgt0  24336  bl2in  24337  blss2ps  24340  blss2  24341  blssps  24361  blss  24362  xmetresbl  24374  lpbl  24440  blcld  24442  stdbdbl  24454  metcnp3  24477  metcnp2  24479  txmetcnp  24484  blval2  24499  nmoix  24666  nmoeq0  24673  icoopnst  24885  iocopnst  24886  xrhmeo  24893  nmhmcn  25069  cphsqrtcl2  25136  cphsqrtcl3  25137  cfil3i  25219  caublcls  25259  bcthlem5  25278  cmetcusp1  25303  cssbn  25325  rrxcph  25342  pjth  25389  ovoliunlem2  25454  volun  25496  volsup2  25556  mbfimaopn2  25608  iblconst  25769  itgconst  25770  dvcnp2  25871  dvcnp2OLD  25872  dvcn  25873  deg1mul3le  26072  deg1tmle  26073  dvdsq1p  26118  ig1peu  26130  ig1pdvds  26135  coeid3  26195  dgrmulc  26227  efcvx  26409  tanord  26497  logdivlti  26579  logccv  26622  recxpcl  26634  cxpeq  26717  ang180  26774  isosctrlem2  26779  cxp2lim  26937  amgm  26951  muval1  27093  dvdssqf  27098  mumullem2  27140  mumul  27141  bcmono  27238  lgsfcl2  27264  lgsdilem  27285  lgsdirprm  27292  lgsdir  27293  lgsdi  27295  lgsne0  27296  padicabv  27591  nosep1o  27643  nosep2o  27644  nosepssdm  27648  nolt02olem  27656  nosupres  27669  nosupbnd1lem1  27670  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  nosupbnd2  27678  noinfres  27684  noinfbnd1lem1  27685  noinfbnd1lem4  27688  noinfbnd1lem6  27690  noinfbnd2  27693  noetasuplem3  27697  noetalem1  27703  scutbdaybnd  27777  sltlpss  27862  slelss  27863  coinitsslt  27870  addsass  27955  addsdi  28098  mulsass  28109  norecdiv  28133  brbtwn2  28830  colinearalglem1  28831  colinearalg  28835  axcgrtr  28840  axsegconlem8  28849  axsegconlem9  28850  axsegconlem10  28851  axcontlem8  28896  axcontlem10  28898  elntg2  28910  vtxdlfuhgr1v  29405  umgr2wlk  29877  erclwwlksym  29948  clwwlkfo  29977  clwwlkext2edg  29983  erclwwlknsym  29997  clwwlknon1  30024  numclwwlk2lem1  30303  numclwwlk5  30315  frgrregord13  30323  nvmul0or  30577  ipval2lem2  30631  lnomul  30687  shless  31286  shlej1  31287  pjspansn  31504  hoadddi  31730  kbmul  31882  homco2  31904  kbass2  32044  eliccelico  32700  elicoelioo  32701  iocinioc2  32702  iocinif  32704  swrdrn2  32876  xrge0adddir  32959  xrge0npcan  32961  archiabl  33142  ress1r  33175  pidlnz  33337  grplsm0l  33364  intlidl  33381  ssmxidl  33435  pstmfval  33873  fmcncfil  33908  zrhnm  33944  qqhnm  33967  measvunilem  34189  volfiniune  34207  dya2iocnrect  34259  sibfinima  34317  probun  34397  probinc  34399  cndprob01  34413  signstfvp  34549  bnj517  34862  bnj594  34889  pconnpi1  35205  cvmsss2  35242  mrsubcv  35478  msubvrs  35528  br6  35720  br4  35721  cgrcomim  35953  cgrtriv  35966  cgrextend  35972  segconeq  35974  btwntriv2  35976  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  trisegint  35992  cgrsub  36009  cgrxfr  36019  btwnxfr  36020  lineext  36040  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  segcon2  36069  brsegle  36072  brsegle2  36073  segletr  36078  segleantisym  36079  seglelin  36080  outsideofeu  36095  lineunray  36111  lineelsb2  36112  ivthALT  36299  weiunpo  36429  weiunso  36430  weiunfr  36431  weiunse  36432  lindsenlbs  37585  areacirc  37683  cocanfo  37689  upixp  37699  ismtyima  37773  rrndstprj2  37801  zerdivemp1x  37917  lsatfixedN  38973  lssat  38980  eqlkr  39063  eqlkr2  39064  lkrlsp  39066  lshpkrlem4  39077  opposet  39145  cvrcon3b  39241  cvrcmp  39247  atlen0  39274  atnle  39281  atlatmstc  39283  cvlatexch3  39302  cvlsupr2  39307  hlsupr2  39352  hlrelat2  39368  cvrexchlem  39384  lnnat  39392  atcvrj2b  39397  atle  39401  atexchcvrN  39405  atbtwn  39411  athgt  39421  3dimlem3  39426  3dim1  39432  1cvratlt  39439  1cvrjat  39440  ps-1  39442  ps-2  39443  3atlem3  39450  3atlem5  39452  3atlem7  39454  llni  39473  llni2  39477  atcvrlln2  39484  llnexatN  39486  llncmp  39487  2llnmat  39489  2at0mat0  39490  lplni  39497  lplnnle2at  39506  2atnelpln  39509  lplnllnneN  39521  llncvrlpln2  39522  2lplnmN  39524  2llnmj  39525  lplncmp  39527  lplnexatN  39528  lplnexllnN  39529  2llnm3N  39534  lvoli  39540  lvoli3  39542  islvol2aN  39557  4atlem0a  39558  4atlem3  39561  4atlem3a  39562  4atlem4a  39564  4atlem4b  39565  4atlem4c  39566  4atlem4d  39567  4atlem10b  39570  4atlem11  39574  4atlem12  39577  lplncvrlvol2  39580  lvolcmp  39582  2lplnmj  39587  islinei  39705  pmapglbx  39734  linepmap  39740  lneq2at  39743  lnjatN  39745  lncvrat  39747  lncmp  39748  2llnma3r  39753  elpaddatriN  39768  elpaddat  39769  paddcom  39778  paddss1  39782  paddss2  39783  paddss12  39784  paddasslem6  39790  paddasslem7  39791  paddasslem8  39792  paddasslem9  39793  paddasslem15  39799  pmodlem2  39812  pmodl42N  39816  pmapjoin  39817  llnmod1i2  39825  2polcon4bN  39883  polcon2bN  39885  poml4N  39918  poml6N  39920  osumcllem1N  39921  osumcllem2N  39922  osumcllem11N  39931  osumclN  39932  pmapojoinN  39933  pexmidlem2N  39936  pexmidlem3N  39937  pexmidlem4N  39938  pexmidlem6N  39940  pexmidlem7N  39941  pl42lem2N  39945  pl42lem3N  39946  pl42lem4N  39947  pl42N  39948  lhpexle2lem  39974  lhpexle3lem  39976  lhpexle3  39977  lhpmcvr3  39990  lhp2at0nle  40000  lhprelat3N  40005  4atex  40041  4atex2  40042  lauteq  40060  lautco  40062  ltrncoidN  40093  ltrneq2  40113  ltrnnidn  40139  ltrnideq  40140  trlnid  40144  ltrnatlw  40148  trlnle  40151  trlval3  40152  trlval4  40153  cdlemc  40162  cdlemd5  40167  cdlemd9  40171  ltrneq3  40173  cdleme0moN  40190  cdleme20  40289  cdleme21j  40301  cdleme21  40302  cdleme27cl  40331  cdlemefrs29bpre0  40361  cdlemefs27cl  40378  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme32d  40409  cdleme32f  40411  cdleme32le  40412  cdleme35h2  40422  cdleme38n  40429  cdleme40m  40432  cdleme41snaw  40441  cdleme42ke  40450  cdleme17d3  40461  cdleme48fvg  40465  cdlemeg46fvcl  40471  cdlemeg46fgN  40499  cdleme48gfv1  40501  cdleme48fgv  40503  cdleme50trn3  40518  trlord  40534  ltrniotavalbN  40549  cdlemb3  40571  cdlemg6c  40585  cdlemg6  40588  cdlemg7N  40591  cdlemg8c  40594  cdlemg8  40596  cdlemg11a  40602  cdlemg11b  40607  cdlemg12e  40612  cdlemg15a  40620  cdlemg15  40621  cdlemg16  40622  cdlemg16z  40624  cdlemg16zz  40625  cdlemg17dN  40628  cdlemg18a  40643  cdlemg20  40650  cdlemg22  40652  cdlemg24  40653  cdlemg37  40654  cdlemg31d  40665  cdlemg29  40670  cdlemg33b  40672  cdlemg33  40676  cdlemg38  40680  cdlemg39  40681  cdlemg40  40682  trlco  40692  trlcone  40693  cdlemg42  40694  cdlemg44b  40697  ltrncom  40703  trljco  40705  tendococl  40737  tendoplcl  40746  tendoplcom  40747  cdlemj2  40787  cdlemj3  40788  tendoid0  40790  tendoconid  40794  tendotr  40795  cdlemk25-3  40869  cdlemk26b-3  40870  cdlemk34  40875  cdlemk36  40878  cdlemk38  40880  cdlemkid4  40899  cdlemk35s-id  40903  cdlemk39s-id  40905  cdlemk19x  40908  cdlemk53  40922  cdlemk55  40926  cdlemk55u  40931  cdlemk39u  40933  cdlemk19u  40935  cdlemk56  40936  tendoex  40940  cdleml3N  40943  cdleml5N  40945  tendospcanN  40988  cdlemm10N  41083  cdlemn11pre  41175  dihord2pre  41190  dihvalcqpre  41200  dihopelvalcpre  41213  dihord6apre  41221  dihord5b  41224  dihord5apre  41227  dihord  41229  dihmeetlem1N  41255  dihglblem5apreN  41256  dihglblem3N  41260  dihmeetlem2N  41264  dihglbcpreN  41265  dihmeetbN  41268  dihmeetlem4preN  41271  dihmeetlem5  41273  dihmeetlem7N  41275  dihmeetlem10N  41281  dihmeetlem11N  41282  dihmeetlem12N  41283  dihmeetlem13N  41284  dihmeetlem15N  41286  dihmeetlem16N  41287  dihmeetlem17N  41288  dihmeetlem18N  41289  dihmeetlem19N  41290  dihmeetALTN  41292  dih1dimatlem0  41293  dihlspsnssN  41297  dihlspsnat  41298  mapdh8ad  41744  hdmap14lem14  41846  hgmapvvlem3  41890  aks6d1c6isolem1  42133  dvdsexpnn  42329  resubcan2  42378  mzprename  42719  eldioph2lem1  42730  lzunuz  42738  rencldnfi  42791  pellexlem2  42800  infmrgelbi  42848  pellfundglb  42855  pellfund14gap  42857  qirropth  42878  rmxycomplete  42888  congadd  42937  acongeq  42954  jm2.19  42964  jm2.23  42967  jm2.20nn  42968  jm2.27  42979  jm3.1  42991  aomclem6  43030  lnmepi  43056  lmhmfgsplit  43057  lmhmlnmsplit  43058  pwssplit4  43060  hbtlem2  43095  hbtlem5  43099  dgraa0p  43120  proot1hash  43166  iocunico  43182  oasubex  43257  oege1  43277  relexpxpmin  43688  brtrclfv2  43698  ntrclsiso  44038  ntrclskb  44040  ntrclsk3  44041  k0004lem3  44120  grur1cld  44204  ismnu  44233  grumnudlem  44257  suprnmpt  45146  wessf1ornlem  45157  projf1o  45169  snunioo1  45489  iccintsng  45500  lptre2pt  45617  limcleqr  45621  fnlimfvre  45651  limsupgtlem  45754  volioc  45949  iblspltprt  45950  stoweidlem19  45996  stoweidlem20  45997  stoweidlem22  45999  stoweidlem28  46005  stoweidlem34  46011  stoweidlem44  46021  stoweidlem60  46037  wallispilem3  46044  fourierdlem41  46125  fourierdlem42  46126  fourierdlem49  46132  fourierdlem51  46134  fourierdlem54  46137  fourierdlem74  46157  fourierdlem97  46180  caratheodorylem2  46504  ovnsubaddlem2  46548  hspmbllem2  46604  smflimmpt  46787  smflimsupmpt  46806  smfliminfmpt  46809  funfocofob  47055  fzopredsuc  47300  imasetpreimafvbijlemfv  47364  iccpartigtl  47385  lighneal  47573  oexpnegALTV  47639  oexpnegnz  47640  tgblthelfgott  47777  clnbgrgrim  47895  uhgrimgrlim  47947  gpgusgralem  48008  lidldomn1  48154  ofaddmndmap  48266  lincdifsn  48348  lincellss  48350  lincresunit3lem3  48398  islindeps2  48407  lindssnlvec  48410  fdivmptf  48469  refdivmptf  48470  rrx2linest  48670  itsclc0yqsollem1  48690  itsclc0b  48700  itsclquadb  48704  itscnhlinecirc02plem3  48712  diag1  49163  setc1onsubc  49427