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  3590  2nreu  4393  predtrss  6274  frpomin  6292  f1prex  7224  cocan1  7231  weniso  7294  frrlem4  8225  frrlem10  8231  fprlem1  8236  smogt  8293  smocdmdom  8294  omeulem1  8503  nnmord  8553  nnmword  8554  naddasslem1  8615  naddasslem2  8616  difsnen  8979  enfixsn  9006  mapunen  9066  ac6sfi  9175  fipreima  9249  elfiun  9321  ordiso2  9408  wemaplem2  9440  en2eqpr  9905  indcardi  9939  fodomfi2  9958  iunfictbso  10012  infmap2  10115  cofsmo  10167  cfsmolem  10168  coftr  10171  fin23lem11  10215  fincssdom  10221  fin23lem26  10223  isf32lem9  10259  ac6num  10377  gchdomtri  10527  gchpwdom  10568  winainflem  10591  tskuni  10681  gruima  10700  gruf  10709  grudomon  10715  elnpi  10886  distrlem4pr  10924  prlem934  10931  addcan  11304  addcan2  11305  divmulass  11806  divmulasscom  11807  ltmul1a  11977  suprleub  12095  supmul1  12098  suprzcl  12559  uzsupss  12840  xleadd1a  13154  xlesubadd  13164  xmulasslem3  13187  xlemul2a  13190  xadddilem  13195  xadddi2  13198  ixxun  13263  icoshftf1o  13376  ioounsn  13379  snunioc  13382  lincmb01cmp  13397  iccf1o  13398  nn0p1elfzo  13604  fzofzim  13611  fzoopth  13664  ltexp2a  14075  leexp2  14080  ltexp2r  14082  exple1  14086  expnlbnd2  14143  fun2dmnop0  14413  ccatass  14498  swrdswrdlem  14613  ccatopth  14625  repswpfx  14694  2cshw  14722  cshimadifsn  14738  cshimadifsn0  14739  cshco  14745  repsco  14749  s2f1o  14825  limsupgre  15390  addcn2  15503  mulcn2  15505  ntrivcvgmul  15811  binomrisefac  15951  dvdsmodexp  16173  dvdsadd2b  16219  dvdsexp2im  16240  dvdsmod  16242  oexpneg  16258  sadass  16384  gcdass  16460  rplpwr  16471  lcmfunsnlem1  16550  coprmdvds2  16567  rpmulgcd2  16569  qredeq  16570  rpdvds  16573  cncongr2  16581  rpexp  16635  prmdiveq  16699  hashgcdlem  16701  odzdvds  16709  modprmn0modprm0  16721  coprimeprodsq2  16723  pythagtriplem3  16732  pcdvdsb  16783  pcgcd1  16791  qexpz  16815  pockthg  16820  vdwnnlem1  16909  0ram  16934  ramz2  16938  lubss  18421  lubun  18423  clatleglb  18426  clatglbss  18427  mrelatglb  18468  isnsgrp  18633  issubmnd  18671  ress0g  18672  mhmvlin  18711  gsumccat  18751  frmdss2  18773  submefmnd  18805  mulgneg  19007  mulgdirlem  19020  submmulg  19033  subgmulg  19055  nmzsubg  19079  ghmmulg  19142  gsmsymgreqlem1  19344  pmtrfb  19379  psgnunilem4  19411  odmodnn0  19454  odnncl  19459  odmod  19460  odmulgid  19468  odmulgeq  19471  odf1o1  19486  odf1o2  19487  odngen  19491  gexdvdsi  19497  pgpfi1  19509  odcau  19518  subgslw  19530  fislw  19539  lsmssv  19557  lsmless1x  19558  lsmless2x  19559  lsmsubm  19567  lsmmod  19589  lsmmod2  19590  efgred  19662  cntzcmn  19754  ghmplusg  19760  odadd1  19762  odadd2  19763  odadd  19764  lsmcomx  19770  gsumconst  19848  ablsimpgprmd  20031  srg1zr  20135  ring1eq0  20218  mulgass2  20229  rngisom1  20386  rhmdvdsr  20425  isabvd  20729  rmodislmodlem  20864  rmodislmod  20865  lssintcl  20899  0lmhm  20976  lmhmvsca  20981  reslmhm2b  20990  pwssplit1  20995  pwssplit3  20997  lspfixed  21067  lspsnat  21084  rnglidlrng  21186  2idlcpblrng  21210  lidldvgen  21273  xrsdsreclblem  21351  regsumsupp  21561  obselocv  21667  uvcresum  21732  frlmsslsp  21735  frlmup4  21740  lindff1  21759  f1lindf  21761  lsslindf  21769  islindf4  21777  lbslcic  21780  issubassa  21806  evlsval2  22023  psrplusgpropd  22149  coe1subfv  22181  coe1mul2  22184  mpomatmul  22362  mamutpos  22374  scmatscmide  22423  mavmulsolcl  22467  marrepcl  22480  mdetdiag  22515  mdetunilem1  22528  mdetunilem3  22530  mdetunilem7  22534  mdetunilem9  22536  mdetmul  22539  slesolinvbi  22597  m2pmfzmap  22663  pmatcollpwlem  22696  pmatcollpw  22697  mp2pm2mplem4  22725  chpdmatlem3  22756  chfacfisfcpmat  22771  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  chfacfpmmulgsum2  22781  cayhamlem1  22782  cpmidpmatlem2  22787  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  riinopn  22824  neiint  23020  topssnei  23040  restntr  23098  iscnp4  23179  cnconst2  23199  cnrest2  23202  cnprest2  23206  cnpdis  23209  cnt0  23262  cnt1  23266  cnhaus  23270  ordthauslem  23299  cncmp  23308  fiuncmp  23320  sscmp  23321  hauscmp  23323  cnconn  23338  unconn  23345  nlly2i  23392  llynlly  23393  nllyidm  23405  finlocfin  23436  ptrescn  23555  xkococnlem  23575  qtopss  23631  kqfvima  23646  r0cld  23654  ordthmeolem  23717  fbssint  23754  fmf  23861  fmss  23862  elfm  23863  rnelfmlem  23868  rnelfm  23869  fmco  23877  flimss2  23888  flimss1  23889  flimrest  23899  flftg  23912  cnpflf2  23916  cnpflf  23917  flfcnp  23920  supnfcls  23936  fclsss1  23938  fclsss2  23939  fcfnei  23951  fcfelbas  23952  cnpfcfi  23956  subgntr  24023  opnsubg  24024  cldsubg  24027  ghmcnp  24031  utop2nei  24166  neipcfilu  24211  bldisj  24314  blgt0  24315  bl2in  24316  blss2ps  24319  blss2  24320  blssps  24340  blss  24341  xmetresbl  24353  lpbl  24419  blcld  24421  stdbdbl  24433  metcnp3  24456  metcnp2  24458  txmetcnp  24463  blval2  24478  nmoix  24645  nmoeq0  24652  icoopnst  24864  iocopnst  24865  xrhmeo  24872  nmhmcn  25048  cphsqrtcl2  25114  cphsqrtcl3  25115  cfil3i  25197  caublcls  25237  bcthlem5  25256  cmetcusp1  25281  cssbn  25303  rrxcph  25320  pjth  25367  ovoliunlem2  25432  volun  25474  volsup2  25534  mbfimaopn2  25586  iblconst  25747  itgconst  25748  dvcnp2  25849  dvcnp2OLD  25850  dvcn  25851  deg1mul3le  26050  deg1tmle  26051  dvdsq1p  26096  ig1peu  26108  ig1pdvds  26113  coeid3  26173  dgrmulc  26205  efcvx  26387  tanord  26475  logdivlti  26557  logccv  26600  recxpcl  26612  cxpeq  26695  ang180  26752  isosctrlem2  26757  cxp2lim  26915  amgm  26929  muval1  27071  dvdssqf  27076  mumullem2  27118  mumul  27119  bcmono  27216  lgsfcl2  27242  lgsdilem  27263  lgsdirprm  27270  lgsdir  27271  lgsdi  27273  lgsne0  27274  padicabv  27569  nosep1o  27621  nosep2o  27622  nosepssdm  27626  nolt02olem  27634  nosupres  27647  nosupbnd1lem1  27648  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd1lem6  27653  nosupbnd2  27656  noinfres  27662  noinfbnd1lem1  27663  noinfbnd1lem4  27666  noinfbnd1lem6  27668  noinfbnd2  27671  noetasuplem3  27675  noetalem1  27681  scutbdaybnd  27757  sltlpss  27854  slelss  27855  coinitsslt  27864  addsass  27949  addsdi  28095  mulsass  28106  norecdiv  28130  brbtwn2  28885  colinearalglem1  28886  colinearalg  28890  axcgrtr  28895  axsegconlem8  28904  axsegconlem9  28905  axsegconlem10  28906  axcontlem8  28951  axcontlem10  28953  elntg2  28965  vtxdlfuhgr1v  29460  umgr2wlk  29929  erclwwlksym  30003  clwwlkfo  30032  clwwlkext2edg  30038  erclwwlknsym  30052  clwwlknon1  30079  numclwwlk2lem1  30358  numclwwlk5  30370  frgrregord13  30378  nvmul0or  30632  ipval2lem2  30686  lnomul  30742  shless  31341  shlej1  31342  pjspansn  31559  hoadddi  31785  kbmul  31937  homco2  31959  kbass2  32099  eliccelico  32764  elicoelioo  32765  iocinioc2  32766  iocinif  32768  swrdrn2  32942  xrge0adddir  33006  xrge0npcan  33008  archiabl  33174  ress1r  33208  pidlnz  33348  grplsm0l  33375  intlidl  33392  ssmxidl  33446  pstmfval  33930  fmcncfil  33965  zrhnm  34001  qqhnm  34024  measvunilem  34246  volfiniune  34264  dya2iocnrect  34315  sibfinima  34373  probun  34453  probinc  34455  cndprob01  34469  signstfvp  34605  bnj517  34918  bnj594  34945  fissorduni  35122  pconnpi1  35302  cvmsss2  35339  mrsubcv  35575  msubvrs  35625  br6  35822  br4  35823  cgrcomim  36054  cgrtriv  36067  cgrextend  36073  segconeq  36075  btwntriv2  36077  btwnintr  36084  btwnexch3  36085  btwnouttr2  36087  trisegint  36093  cgrsub  36110  cgrxfr  36120  btwnxfr  36121  lineext  36141  btwnconn1lem13  36164  btwnconn1lem14  36165  btwnconn3  36168  segcon2  36170  brsegle  36173  brsegle2  36174  segletr  36179  segleantisym  36180  seglelin  36181  outsideofeu  36196  lineunray  36212  lineelsb2  36213  ivthALT  36400  weiunpo  36530  weiunso  36531  weiunfr  36532  weiunse  36533  lindsenlbs  37675  areacirc  37773  cocanfo  37779  upixp  37789  ismtyima  37863  rrndstprj2  37891  zerdivemp1x  38007  lsatfixedN  39128  lssat  39135  eqlkr  39218  eqlkr2  39219  lkrlsp  39221  lshpkrlem4  39232  opposet  39300  cvrcon3b  39396  cvrcmp  39402  atlen0  39429  atnle  39436  atlatmstc  39438  cvlatexch3  39457  cvlsupr2  39462  hlsupr2  39506  hlrelat2  39522  cvrexchlem  39538  lnnat  39546  atcvrj2b  39551  atle  39555  atexchcvrN  39559  atbtwn  39565  athgt  39575  3dimlem3  39580  3dim1  39586  1cvratlt  39593  1cvrjat  39594  ps-1  39596  ps-2  39597  3atlem3  39604  3atlem5  39606  3atlem7  39608  llni  39627  llni2  39631  atcvrlln2  39638  llnexatN  39640  llncmp  39641  2llnmat  39643  2at0mat0  39644  lplni  39651  lplnnle2at  39660  2atnelpln  39663  lplnllnneN  39675  llncvrlpln2  39676  2lplnmN  39678  2llnmj  39679  lplncmp  39681  lplnexatN  39682  lplnexllnN  39683  2llnm3N  39688  lvoli  39694  lvoli3  39696  islvol2aN  39711  4atlem0a  39712  4atlem3  39715  4atlem3a  39716  4atlem4a  39718  4atlem4b  39719  4atlem4c  39720  4atlem4d  39721  4atlem10b  39724  4atlem11  39728  4atlem12  39731  lplncvrlvol2  39734  lvolcmp  39736  2lplnmj  39741  islinei  39859  pmapglbx  39888  linepmap  39894  lneq2at  39897  lnjatN  39899  lncvrat  39901  lncmp  39902  2llnma3r  39907  elpaddatriN  39922  elpaddat  39923  paddcom  39932  paddss1  39936  paddss2  39937  paddss12  39938  paddasslem6  39944  paddasslem7  39945  paddasslem8  39946  paddasslem9  39947  paddasslem15  39953  pmodlem2  39966  pmodl42N  39970  pmapjoin  39971  llnmod1i2  39979  2polcon4bN  40037  polcon2bN  40039  poml4N  40072  poml6N  40074  osumcllem1N  40075  osumcllem2N  40076  osumcllem11N  40085  osumclN  40086  pmapojoinN  40087  pexmidlem2N  40090  pexmidlem3N  40091  pexmidlem4N  40092  pexmidlem6N  40094  pexmidlem7N  40095  pl42lem2N  40099  pl42lem3N  40100  pl42lem4N  40101  pl42N  40102  lhpexle2lem  40128  lhpexle3lem  40130  lhpexle3  40131  lhpmcvr3  40144  lhp2at0nle  40154  lhprelat3N  40159  4atex  40195  4atex2  40196  lauteq  40214  lautco  40216  ltrncoidN  40247  ltrneq2  40267  ltrnnidn  40293  ltrnideq  40294  trlnid  40298  ltrnatlw  40302  trlnle  40305  trlval3  40306  trlval4  40307  cdlemc  40316  cdlemd5  40321  cdlemd9  40325  ltrneq3  40327  cdleme0moN  40344  cdleme20  40443  cdleme21j  40455  cdleme21  40456  cdleme27cl  40485  cdlemefrs29bpre0  40515  cdlemefs27cl  40532  cdlemefs32sn1aw  40533  cdleme43fsv1snlem  40539  cdleme32d  40563  cdleme32f  40565  cdleme32le  40566  cdleme35h2  40576  cdleme38n  40583  cdleme40m  40586  cdleme41snaw  40595  cdleme42ke  40604  cdleme17d3  40615  cdleme48fvg  40619  cdlemeg46fvcl  40625  cdlemeg46fgN  40653  cdleme48gfv1  40655  cdleme48fgv  40657  cdleme50trn3  40672  trlord  40688  ltrniotavalbN  40703  cdlemb3  40725  cdlemg6c  40739  cdlemg6  40742  cdlemg7N  40745  cdlemg8c  40748  cdlemg8  40750  cdlemg11a  40756  cdlemg11b  40761  cdlemg12e  40766  cdlemg15a  40774  cdlemg15  40775  cdlemg16  40776  cdlemg16z  40778  cdlemg16zz  40779  cdlemg17dN  40782  cdlemg18a  40797  cdlemg20  40804  cdlemg22  40806  cdlemg24  40807  cdlemg37  40808  cdlemg31d  40819  cdlemg29  40824  cdlemg33b  40826  cdlemg33  40830  cdlemg38  40834  cdlemg39  40835  cdlemg40  40836  trlco  40846  trlcone  40847  cdlemg42  40848  cdlemg44b  40851  ltrncom  40857  trljco  40859  tendococl  40891  tendoplcl  40900  tendoplcom  40901  cdlemj2  40941  cdlemj3  40942  tendoid0  40944  tendoconid  40948  tendotr  40949  cdlemk25-3  41023  cdlemk26b-3  41024  cdlemk34  41029  cdlemk36  41032  cdlemk38  41034  cdlemkid4  41053  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk19x  41062  cdlemk53  41076  cdlemk55  41080  cdlemk55u  41085  cdlemk39u  41087  cdlemk19u  41089  cdlemk56  41090  tendoex  41094  cdleml3N  41097  cdleml5N  41099  tendospcanN  41142  cdlemm10N  41237  cdlemn11pre  41329  dihord2pre  41344  dihvalcqpre  41354  dihopelvalcpre  41367  dihord6apre  41375  dihord5b  41378  dihord5apre  41381  dihord  41383  dihmeetlem1N  41409  dihglblem5apreN  41410  dihglblem3N  41414  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetbN  41422  dihmeetlem4preN  41425  dihmeetlem5  41427  dihmeetlem7N  41429  dihmeetlem10N  41435  dihmeetlem11N  41436  dihmeetlem12N  41437  dihmeetlem13N  41438  dihmeetlem15N  41440  dihmeetlem16N  41441  dihmeetlem17N  41442  dihmeetlem18N  41443  dihmeetlem19N  41444  dihmeetALTN  41446  dih1dimatlem0  41447  dihlspsnssN  41451  dihlspsnat  41452  mapdh8ad  41898  hdmap14lem14  42000  hgmapvvlem3  42044  aks6d1c6isolem1  42287  dvdsexpnn  42451  resubcan2  42506  mzprename  42866  eldioph2lem1  42877  lzunuz  42885  rencldnfi  42938  pellexlem2  42947  infmrgelbi  42995  pellfundglb  43002  pellfund14gap  43004  qirropth  43025  rmxycomplete  43034  congadd  43083  acongeq  43100  jm2.19  43110  jm2.23  43113  jm2.20nn  43114  jm2.27  43125  jm3.1  43137  aomclem6  43176  lnmepi  43202  lmhmfgsplit  43203  lmhmlnmsplit  43204  pwssplit4  43206  hbtlem2  43241  hbtlem5  43245  dgraa0p  43266  proot1hash  43312  iocunico  43328  oasubex  43403  oege1  43423  relexpxpmin  43834  brtrclfv2  43844  ntrclsiso  44184  ntrclskb  44186  ntrclsk3  44187  k0004lem3  44266  grur1cld  44349  ismnu  44378  grumnudlem  44402  suprnmpt  45295  wessf1ornlem  45306  projf1o  45318  snunioo1  45636  iccintsng  45647  lptre2pt  45762  limcleqr  45766  fnlimfvre  45796  limsupgtlem  45899  volioc  46094  iblspltprt  46095  stoweidlem19  46141  stoweidlem20  46142  stoweidlem22  46144  stoweidlem28  46150  stoweidlem34  46156  stoweidlem44  46166  stoweidlem60  46182  wallispilem3  46189  fourierdlem41  46270  fourierdlem42  46271  fourierdlem49  46277  fourierdlem51  46279  fourierdlem54  46282  fourierdlem74  46302  fourierdlem97  46325  caratheodorylem2  46649  ovnsubaddlem2  46693  hspmbllem2  46749  smflimmpt  46932  smflimsupmpt  46951  smfliminfmpt  46954  funfocofob  47202  fzopredsuc  47447  imasetpreimafvbijlemfv  47526  iccpartigtl  47547  lighneal  47735  oexpnegALTV  47801  oexpnegnz  47802  tgblthelfgott  47939  clnbgrgrim  48058  uhgrimgrlim  48111  gpgusgralem  48180  lidldomn1  48355  ofaddmndmap  48467  lincdifsn  48549  lincellss  48551  lincresunit3lem3  48599  islindeps2  48608  lindssnlvec  48611  fdivmptf  48666  refdivmptf  48667  rrx2linest  48867  itsclc0yqsollem1  48887  itsclc0b  48897  itsclquadb  48901  itscnhlinecirc02plem3  48909  diag1  49429  setc1onsubc  49727