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  3596  2nreu  4397  predtrss  6274  frpomin  6292  f1prex  7225  cocan1  7232  weniso  7295  frrlem4  8229  frrlem10  8235  fprlem1  8240  smogt  8297  smocdmdom  8298  omeulem1  8507  nnmord  8557  nnmword  8558  naddasslem1  8619  naddasslem2  8620  difsnen  8983  enfixsn  9010  mapunen  9070  ac6sfi  9189  fipreima  9267  elfiun  9339  ordiso2  9426  wemaplem2  9458  en2eqpr  9920  indcardi  9954  fodomfi2  9973  iunfictbso  10027  infmap2  10130  cofsmo  10182  cfsmolem  10183  coftr  10186  fin23lem11  10230  fincssdom  10236  fin23lem26  10238  isf32lem9  10274  ac6num  10392  gchdomtri  10542  gchpwdom  10583  winainflem  10606  tskuni  10696  gruima  10715  gruf  10724  grudomon  10730  elnpi  10901  distrlem4pr  10939  prlem934  10946  addcan  11318  addcan2  11319  divmulass  11820  divmulasscom  11821  ltmul1a  11991  suprleub  12109  supmul1  12112  suprzcl  12574  uzsupss  12859  xleadd1a  13173  xlesubadd  13183  xmulasslem3  13206  xlemul2a  13209  xadddilem  13214  xadddi2  13217  ixxun  13282  icoshftf1o  13395  ioounsn  13398  snunioc  13401  lincmb01cmp  13416  iccf1o  13417  nn0p1elfzo  13623  fzofzim  13630  fzoopth  13683  ltexp2a  14091  leexp2  14096  ltexp2r  14098  exple1  14102  expnlbnd2  14159  fun2dmnop0  14429  ccatass  14513  swrdswrdlem  14628  ccatopth  14640  repswpfx  14709  2cshw  14737  cshimadifsn  14754  cshimadifsn0  14755  cshco  14761  repsco  14765  s2f1o  14841  limsupgre  15406  addcn2  15519  mulcn2  15521  ntrivcvgmul  15827  binomrisefac  15967  dvdsmodexp  16189  dvdsadd2b  16235  dvdsexp2im  16256  dvdsmod  16258  oexpneg  16274  sadass  16400  gcdass  16476  rplpwr  16487  lcmfunsnlem1  16566  coprmdvds2  16583  rpmulgcd2  16585  qredeq  16586  rpdvds  16589  cncongr2  16597  rpexp  16651  prmdiveq  16715  hashgcdlem  16717  odzdvds  16725  modprmn0modprm0  16737  coprimeprodsq2  16739  pythagtriplem3  16748  pcdvdsb  16799  pcgcd1  16807  qexpz  16831  pockthg  16836  vdwnnlem1  16925  0ram  16950  ramz2  16954  lubss  18437  lubun  18439  clatleglb  18442  clatglbss  18443  mrelatglb  18484  isnsgrp  18615  issubmnd  18653  ress0g  18654  mhmvlin  18693  gsumccat  18733  frmdss2  18755  submefmnd  18787  mulgneg  18989  mulgdirlem  19002  submmulg  19015  subgmulg  19037  nmzsubg  19062  ghmmulg  19125  gsmsymgreqlem1  19327  pmtrfb  19362  psgnunilem4  19394  odmodnn0  19437  odnncl  19442  odmod  19443  odmulgid  19451  odmulgeq  19454  odf1o1  19469  odf1o2  19470  odngen  19474  gexdvdsi  19480  pgpfi1  19492  odcau  19501  subgslw  19513  fislw  19522  lsmssv  19540  lsmless1x  19541  lsmless2x  19542  lsmsubm  19550  lsmmod  19572  lsmmod2  19573  efgred  19645  cntzcmn  19737  ghmplusg  19743  odadd1  19745  odadd2  19746  odadd  19747  lsmcomx  19753  gsumconst  19831  ablsimpgprmd  20014  srg1zr  20118  ring1eq0  20201  mulgass2  20212  rngisom1  20369  rhmdvdsr  20411  isabvd  20715  rmodislmodlem  20850  rmodislmod  20851  lssintcl  20885  0lmhm  20962  lmhmvsca  20967  reslmhm2b  20976  pwssplit1  20981  pwssplit3  20983  lspfixed  21053  lspsnat  21070  rnglidlrng  21172  2idlcpblrng  21196  lidldvgen  21259  xrsdsreclblem  21337  regsumsupp  21547  obselocv  21653  uvcresum  21718  frlmsslsp  21721  frlmup4  21726  lindff1  21745  f1lindf  21747  lsslindf  21755  islindf4  21763  lbslcic  21766  issubassa  21792  evlsval2  22010  psrplusgpropd  22136  coe1subfv  22168  coe1mul2  22171  mpomatmul  22349  mamutpos  22361  scmatscmide  22410  mavmulsolcl  22454  marrepcl  22467  mdetdiag  22502  mdetunilem1  22515  mdetunilem3  22517  mdetunilem7  22521  mdetunilem9  22523  mdetmul  22526  slesolinvbi  22584  m2pmfzmap  22650  pmatcollpwlem  22683  pmatcollpw  22684  mp2pm2mplem4  22712  chpdmatlem3  22743  chfacfisfcpmat  22758  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  chfacfpmmulgsum2  22768  cayhamlem1  22769  cpmidpmatlem2  22774  cpmadugsumlemB  22777  cpmadugsumlemC  22778  cpmadugsumlemF  22779  riinopn  22811  neiint  23007  topssnei  23027  restntr  23085  iscnp4  23166  cnconst2  23186  cnrest2  23189  cnprest2  23193  cnpdis  23196  cnt0  23249  cnt1  23253  cnhaus  23257  ordthauslem  23286  cncmp  23295  fiuncmp  23307  sscmp  23308  hauscmp  23310  cnconn  23325  unconn  23332  nlly2i  23379  llynlly  23380  nllyidm  23392  finlocfin  23423  ptrescn  23542  xkococnlem  23562  qtopss  23618  kqfvima  23633  r0cld  23641  ordthmeolem  23704  fbssint  23741  fmf  23848  fmss  23849  elfm  23850  rnelfmlem  23855  rnelfm  23856  fmco  23864  flimss2  23875  flimss1  23876  flimrest  23886  flftg  23899  cnpflf2  23903  cnpflf  23904  flfcnp  23907  supnfcls  23923  fclsss1  23925  fclsss2  23926  fcfnei  23938  fcfelbas  23939  cnpfcfi  23943  subgntr  24010  opnsubg  24011  cldsubg  24014  ghmcnp  24018  utop2nei  24154  neipcfilu  24199  bldisj  24302  blgt0  24303  bl2in  24304  blss2ps  24307  blss2  24308  blssps  24328  blss  24329  xmetresbl  24341  lpbl  24407  blcld  24409  stdbdbl  24421  metcnp3  24444  metcnp2  24446  txmetcnp  24451  blval2  24466  nmoix  24633  nmoeq0  24640  icoopnst  24852  iocopnst  24853  xrhmeo  24860  nmhmcn  25036  cphsqrtcl2  25102  cphsqrtcl3  25103  cfil3i  25185  caublcls  25225  bcthlem5  25244  cmetcusp1  25269  cssbn  25291  rrxcph  25308  pjth  25355  ovoliunlem2  25420  volun  25462  volsup2  25522  mbfimaopn2  25574  iblconst  25735  itgconst  25736  dvcnp2  25837  dvcnp2OLD  25838  dvcn  25839  deg1mul3le  26038  deg1tmle  26039  dvdsq1p  26084  ig1peu  26096  ig1pdvds  26101  coeid3  26161  dgrmulc  26193  efcvx  26375  tanord  26463  logdivlti  26545  logccv  26588  recxpcl  26600  cxpeq  26683  ang180  26740  isosctrlem2  26745  cxp2lim  26903  amgm  26917  muval1  27059  dvdssqf  27064  mumullem2  27106  mumul  27107  bcmono  27204  lgsfcl2  27230  lgsdilem  27251  lgsdirprm  27258  lgsdir  27259  lgsdi  27261  lgsne0  27262  padicabv  27557  nosep1o  27609  nosep2o  27610  nosepssdm  27614  nolt02olem  27622  nosupres  27635  nosupbnd1lem1  27636  nosupbnd1lem4  27639  nosupbnd1lem5  27640  nosupbnd1lem6  27641  nosupbnd2  27644  noinfres  27650  noinfbnd1lem1  27651  noinfbnd1lem4  27654  noinfbnd1lem6  27656  noinfbnd2  27659  noetasuplem3  27663  noetalem1  27669  scutbdaybnd  27744  sltlpss  27840  slelss  27841  coinitsslt  27850  addsass  27935  addsdi  28081  mulsass  28092  norecdiv  28116  brbtwn2  28868  colinearalglem1  28869  colinearalg  28873  axcgrtr  28878  axsegconlem8  28887  axsegconlem9  28888  axsegconlem10  28889  axcontlem8  28934  axcontlem10  28936  elntg2  28948  vtxdlfuhgr1v  29443  umgr2wlk  29912  erclwwlksym  29983  clwwlkfo  30012  clwwlkext2edg  30018  erclwwlknsym  30032  clwwlknon1  30059  numclwwlk2lem1  30338  numclwwlk5  30350  frgrregord13  30358  nvmul0or  30612  ipval2lem2  30666  lnomul  30722  shless  31321  shlej1  31322  pjspansn  31539  hoadddi  31765  kbmul  31917  homco2  31939  kbass2  32079  eliccelico  32733  elicoelioo  32734  iocinioc2  32735  iocinif  32737  swrdrn2  32909  xrge0adddir  32985  xrge0npcan  32987  archiabl  33150  ress1r  33184  pidlnz  33323  grplsm0l  33350  intlidl  33367  ssmxidl  33421  pstmfval  33862  fmcncfil  33897  zrhnm  33933  qqhnm  33956  measvunilem  34178  volfiniune  34196  dya2iocnrect  34248  sibfinima  34306  probun  34386  probinc  34388  cndprob01  34402  signstfvp  34538  bnj517  34851  bnj594  34878  pconnpi1  35209  cvmsss2  35246  mrsubcv  35482  msubvrs  35532  br6  35729  br4  35730  cgrcomim  35962  cgrtriv  35975  cgrextend  35981  segconeq  35983  btwntriv2  35985  btwnintr  35992  btwnexch3  35993  btwnouttr2  35995  trisegint  36001  cgrsub  36018  cgrxfr  36028  btwnxfr  36029  lineext  36049  btwnconn1lem13  36072  btwnconn1lem14  36073  btwnconn3  36076  segcon2  36078  brsegle  36081  brsegle2  36082  segletr  36087  segleantisym  36088  seglelin  36089  outsideofeu  36104  lineunray  36120  lineelsb2  36121  ivthALT  36308  weiunpo  36438  weiunso  36439  weiunfr  36440  weiunse  36441  lindsenlbs  37594  areacirc  37692  cocanfo  37698  upixp  37708  ismtyima  37782  rrndstprj2  37810  zerdivemp1x  37926  lsatfixedN  38987  lssat  38994  eqlkr  39077  eqlkr2  39078  lkrlsp  39080  lshpkrlem4  39091  opposet  39159  cvrcon3b  39255  cvrcmp  39261  atlen0  39288  atnle  39295  atlatmstc  39297  cvlatexch3  39316  cvlsupr2  39321  hlsupr2  39366  hlrelat2  39382  cvrexchlem  39398  lnnat  39406  atcvrj2b  39411  atle  39415  atexchcvrN  39419  atbtwn  39425  athgt  39435  3dimlem3  39440  3dim1  39446  1cvratlt  39453  1cvrjat  39454  ps-1  39456  ps-2  39457  3atlem3  39464  3atlem5  39466  3atlem7  39468  llni  39487  llni2  39491  atcvrlln2  39498  llnexatN  39500  llncmp  39501  2llnmat  39503  2at0mat0  39504  lplni  39511  lplnnle2at  39520  2atnelpln  39523  lplnllnneN  39535  llncvrlpln2  39536  2lplnmN  39538  2llnmj  39539  lplncmp  39541  lplnexatN  39542  lplnexllnN  39543  2llnm3N  39548  lvoli  39554  lvoli3  39556  islvol2aN  39571  4atlem0a  39572  4atlem3  39575  4atlem3a  39576  4atlem4a  39578  4atlem4b  39579  4atlem4c  39580  4atlem4d  39581  4atlem10b  39584  4atlem11  39588  4atlem12  39591  lplncvrlvol2  39594  lvolcmp  39596  2lplnmj  39601  islinei  39719  pmapglbx  39748  linepmap  39754  lneq2at  39757  lnjatN  39759  lncvrat  39761  lncmp  39762  2llnma3r  39767  elpaddatriN  39782  elpaddat  39783  paddcom  39792  paddss1  39796  paddss2  39797  paddss12  39798  paddasslem6  39804  paddasslem7  39805  paddasslem8  39806  paddasslem9  39807  paddasslem15  39813  pmodlem2  39826  pmodl42N  39830  pmapjoin  39831  llnmod1i2  39839  2polcon4bN  39897  polcon2bN  39899  poml4N  39932  poml6N  39934  osumcllem1N  39935  osumcllem2N  39936  osumcllem11N  39945  osumclN  39946  pmapojoinN  39947  pexmidlem2N  39950  pexmidlem3N  39951  pexmidlem4N  39952  pexmidlem6N  39954  pexmidlem7N  39955  pl42lem2N  39959  pl42lem3N  39960  pl42lem4N  39961  pl42N  39962  lhpexle2lem  39988  lhpexle3lem  39990  lhpexle3  39991  lhpmcvr3  40004  lhp2at0nle  40014  lhprelat3N  40019  4atex  40055  4atex2  40056  lauteq  40074  lautco  40076  ltrncoidN  40107  ltrneq2  40127  ltrnnidn  40153  ltrnideq  40154  trlnid  40158  ltrnatlw  40162  trlnle  40165  trlval3  40166  trlval4  40167  cdlemc  40176  cdlemd5  40181  cdlemd9  40185  ltrneq3  40187  cdleme0moN  40204  cdleme20  40303  cdleme21j  40315  cdleme21  40316  cdleme27cl  40345  cdlemefrs29bpre0  40375  cdlemefs27cl  40392  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme32d  40423  cdleme32f  40425  cdleme32le  40426  cdleme35h2  40436  cdleme38n  40443  cdleme40m  40446  cdleme41snaw  40455  cdleme42ke  40464  cdleme17d3  40475  cdleme48fvg  40479  cdlemeg46fvcl  40485  cdlemeg46fgN  40513  cdleme48gfv1  40515  cdleme48fgv  40517  cdleme50trn3  40532  trlord  40548  ltrniotavalbN  40563  cdlemb3  40585  cdlemg6c  40599  cdlemg6  40602  cdlemg7N  40605  cdlemg8c  40608  cdlemg8  40610  cdlemg11a  40616  cdlemg11b  40621  cdlemg12e  40626  cdlemg15a  40634  cdlemg15  40635  cdlemg16  40636  cdlemg16z  40638  cdlemg16zz  40639  cdlemg17dN  40642  cdlemg18a  40657  cdlemg20  40664  cdlemg22  40666  cdlemg24  40667  cdlemg37  40668  cdlemg31d  40679  cdlemg29  40684  cdlemg33b  40686  cdlemg33  40690  cdlemg38  40694  cdlemg39  40695  cdlemg40  40696  trlco  40706  trlcone  40707  cdlemg42  40708  cdlemg44b  40711  ltrncom  40717  trljco  40719  tendococl  40751  tendoplcl  40760  tendoplcom  40761  cdlemj2  40801  cdlemj3  40802  tendoid0  40804  tendoconid  40808  tendotr  40809  cdlemk25-3  40883  cdlemk26b-3  40884  cdlemk34  40889  cdlemk36  40892  cdlemk38  40894  cdlemkid4  40913  cdlemk35s-id  40917  cdlemk39s-id  40919  cdlemk19x  40922  cdlemk53  40936  cdlemk55  40940  cdlemk55u  40945  cdlemk39u  40947  cdlemk19u  40949  cdlemk56  40950  tendoex  40954  cdleml3N  40957  cdleml5N  40959  tendospcanN  41002  cdlemm10N  41097  cdlemn11pre  41189  dihord2pre  41204  dihvalcqpre  41214  dihopelvalcpre  41227  dihord6apre  41235  dihord5b  41238  dihord5apre  41241  dihord  41243  dihmeetlem1N  41269  dihglblem5apreN  41270  dihglblem3N  41274  dihmeetlem2N  41278  dihglbcpreN  41279  dihmeetbN  41282  dihmeetlem4preN  41285  dihmeetlem5  41287  dihmeetlem7N  41289  dihmeetlem10N  41295  dihmeetlem11N  41296  dihmeetlem12N  41297  dihmeetlem13N  41298  dihmeetlem15N  41300  dihmeetlem16N  41301  dihmeetlem17N  41302  dihmeetlem18N  41303  dihmeetlem19N  41304  dihmeetALTN  41306  dih1dimatlem0  41307  dihlspsnssN  41311  dihlspsnat  41312  mapdh8ad  41758  hdmap14lem14  41860  hgmapvvlem3  41904  aks6d1c6isolem1  42147  dvdsexpnn  42306  resubcan2  42361  mzprename  42722  eldioph2lem1  42733  lzunuz  42741  rencldnfi  42794  pellexlem2  42803  infmrgelbi  42851  pellfundglb  42858  pellfund14gap  42860  qirropth  42881  rmxycomplete  42890  congadd  42939  acongeq  42956  jm2.19  42966  jm2.23  42969  jm2.20nn  42970  jm2.27  42981  jm3.1  42993  aomclem6  43032  lnmepi  43058  lmhmfgsplit  43059  lmhmlnmsplit  43060  pwssplit4  43062  hbtlem2  43097  hbtlem5  43101  dgraa0p  43122  proot1hash  43168  iocunico  43184  oasubex  43259  oege1  43279  relexpxpmin  43690  brtrclfv2  43700  ntrclsiso  44040  ntrclskb  44042  ntrclsk3  44043  k0004lem3  44122  grur1cld  44205  ismnu  44234  grumnudlem  44258  suprnmpt  45152  wessf1ornlem  45163  projf1o  45175  snunioo1  45494  iccintsng  45505  lptre2pt  45622  limcleqr  45626  fnlimfvre  45656  limsupgtlem  45759  volioc  45954  iblspltprt  45955  stoweidlem19  46001  stoweidlem20  46002  stoweidlem22  46004  stoweidlem28  46010  stoweidlem34  46016  stoweidlem44  46026  stoweidlem60  46042  wallispilem3  46049  fourierdlem41  46130  fourierdlem42  46131  fourierdlem49  46137  fourierdlem51  46139  fourierdlem54  46142  fourierdlem74  46162  fourierdlem97  46185  caratheodorylem2  46509  ovnsubaddlem2  46553  hspmbllem2  46609  smflimmpt  46792  smflimsupmpt  46811  smfliminfmpt  46814  funfocofob  47063  fzopredsuc  47308  imasetpreimafvbijlemfv  47387  iccpartigtl  47408  lighneal  47596  oexpnegALTV  47662  oexpnegnz  47663  tgblthelfgott  47800  clnbgrgrim  47919  uhgrimgrlim  47972  gpgusgralem  48041  lidldomn1  48216  ofaddmndmap  48328  lincdifsn  48410  lincellss  48412  lincresunit3lem3  48460  islindeps2  48469  lindssnlvec  48472  fdivmptf  48527  refdivmptf  48528  rrx2linest  48728  itsclc0yqsollem1  48748  itsclc0b  48758  itsclquadb  48762  itscnhlinecirc02plem3  48770  diag1  49290  setc1onsubc  49588