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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl11  1267  simpl21  1270  simpl31  1273  simp1l1  1285  simp2l1  1291  simp3l1  1297  3anandirs  1501  rspc3ev  3593  2nreu  4402  predtrss  6325  frpomin  6343  f1prex  7292  cocan1  7299  weniso  7364  frrlem4  8307  frrlem10  8313  fprlem1  8318  smogt  8375  smocdmdom  8376  omeulem1  8590  nnmord  8641  nnmword  8642  naddasslem1  8704  naddasslem2  8705  difsnen  9078  enfixsn  9105  mapunen  9165  ac6sfi  9275  fissorduni  9282  fipreima  9347  elfiun  9422  ordiso2  9509  wemaplem2  9541  en2eqpr  10086  indcardi  10120  fodomfi2  10139  iunfictbso  10193  infmap2  10295  cofsmo  10347  cfsmolem  10348  coftr  10351  fin23lem11  10395  fincssdom  10401  fin23lem26  10403  isf32lem9  10439  ac6num  10557  gchdomtri  10714  gchpwdom  10755  winainflem  10778  tskuni  10868  gruima  10887  gruf  10896  grudomon  10902  elnpi  11073  distrlem4pr  11111  prlem934  11118  addcan  11494  addcan2  11495  divmulass  11997  divmulasscom  11998  ltmul1a  12166  suprleub  12283  supmul1  12286  suprzcl  12779  uzsupss  13067  xleadd1a  13383  xlesubadd  13393  xmulasslem3  13416  xlemul2a  13419  xadddilem  13424  xadddi2  13427  ixxun  13492  icoshftf1o  13605  ioounsn  13608  snunioc  13611  lincmb01cmp  13626  iccf1o  13627  nn0p1elfzo  13837  fzofzim  13844  fzoopth  13897  ltexp2a  14309  leexp2  14314  ltexp2r  14316  exple1  14320  expnlbnd2  14378  fun2dmnop0  14649  ccatass  14734  swrdswrdlem  14853  ccatopth  14865  repswpfx  14936  2cshw  14964  cshimadifsn  14980  cshimadifsn0  14981  cshco  14987  repsco  14991  s2f1o  15067  limsupgre  15648  addcn2  15761  mulcn2  15763  ntrivcvgmul  16071  binomrisefac  16208  dvdsmodexp  16430  dvdsadd2b  16476  dvdsexp2im  16497  dvdsmod  16499  oexpneg  16515  sadass  16641  gcdass  16720  rplpwr  16732  dvdsexpnn  16740  lcmfunsnlem1  16812  coprmdvds2  16829  rpmulgcd2  16831  qredeq  16832  rpdvds  16835  cncongr2  16843  rpexp  16898  prmdiveq  16963  hashgcdlem  16965  odzdvds  16973  modprmn0modprm0  16985  coprimeprodsq2  16987  pythagtriplem3  16996  pcdvdsb  17047  pcgcd1  17055  qexpz  17079  pockthg  17084  vdwnnlem1  17173  0ram  17198  ramz2  17202  lubss  18687  lubun  18689  clatleglb  18692  clatglbss  18693  mrelatglb  18734  isnsgrp  18912  issubmnd  18953  ress0gOLD  18955  mhmvlin  18996  gsumccat  19037  frmdss2  19059  submefmnd  19091  mulgneg  19302  mulgdirlem  19315  submmulg  19328  subgmulg  19351  nmzsubg  19375  ghmmulg  19442  gsmsymgreqlem1  19644  pmtrfb  19679  psgnunilem4  19711  odmodnn0  19754  odnncl  19759  odmod  19760  odmulgid  19768  odmulgeq  19771  odf1o1  19786  odf1o2  19787  odngen  19791  gexdvdsi  19797  pgpfi1  19809  odcau  19818  subgslw  19830  fislw  19839  lsmssv  19857  lsmless1x  19858  lsmless2x  19859  lsmsubm  19867  lsmmod  19889  lsmmod2  19890  efgred  19962  cntzcmn  20054  ghmplusg  20060  odadd1  20062  odadd2  20063  odadd  20064  lsmcomx  20070  gsumconst  20148  ablsimpgprmd  20331  ring1eq0  20529  mulgass2  20540  rngisom1  20696  rhmdvdsr  20758  isabvd  21069  rmodislmodlem  21204  rmodislmod  21205  lssintcl  21239  0lmhm  21315  lmhmvsca  21320  reslmhm2b  21329  pwssplit1  21334  pwssplit3  21336  lspfixed  21406  lspsnat  21423  unichnlidl  21516  pidlnz  21528  rnglidlrng  21535  2idlcpblrng  21565  lidldvgen  21658  xrsdsreclblem  21719  regsumsupp  21928  obselocv  22034  uvcresum  22099  frlmsslsp  22102  frlmup4  22107  lindff1  22126  f1lindf  22128  lsslindf  22136  islindf4  22144  lbslcic  22147  lindsenlbs  22157  issubassa  22175  evlsval2  22396  psrplusgpropd  22553  coe1subfv  22585  coe1mul2  22588  mpomatmul  22761  mamutpos  22773  scmatscmide  22822  mavmulsolcl  22866  marrepcl  22879  mdetdiag  22914  mdetunilem1  22927  mdetunilem3  22929  mdetunilem7  22933  mdetunilem9  22935  mdetmul  22938  slesolinvbi  22999  m2pmfzmap  23065  pmatcollpwlem  23098  pmatcollpw  23099  mp2pm2mplem4  23127  chpdmatlem3  23158  chfacfisfcpmat  23173  chfacfscmulgsum  23178  chfacfpmmulgsum  23182  chfacfpmmulgsum2  23183  cayhamlem1  23184  cpmidpmatlem2  23189  cpmadugsumlemB  23192  cpmadugsumlemC  23193  cpmadugsumlemF  23194  riinopn  23226  neiint  23422  topssnei  23442  restntr  23500  iscnp4  23581  cnconst2  23601  cnrest2  23604  cnprest2  23608  cnpdis  23611  cnt0  23664  cnt1  23668  cnhaus  23672  ordthauslem  23701  cncmp  23710  fiuncmp  23722  sscmp  23723  hauscmp  23725  cnconn  23740  unconn  23747  nlly2i  23795  llynlly  23796  nllyidm  23808  finlocfin  23839  ptrescn  23958  xkococnlem  23978  qtopss  24034  kqfvima  24049  r0cld  24057  ordthmeolem  24120  fbssint  24157  fmf  24264  fmss  24265  elfm  24266  rnelfmlem  24271  rnelfm  24272  fmco  24280  flimss2  24291  flimss1  24292  flimrest  24302  flftg  24315  cnpflf2  24319  cnpflf  24320  flfcnp  24323  supnfcls  24339  fclsss1  24341  fclsss2  24342  fcfnei  24354  fcfelbas  24355  cnpfcfi  24359  subgntr  24426  opnsubg  24427  cldsubg  24430  ghmcnp  24434  utop2nei  24569  neipcfilu  24614  bldisj  24717  blgt0  24718  bl2in  24719  blss2ps  24722  blss2  24723  blssps  24743  blss  24744  xmetresbl  24756  lpbl  24822  blcld  24824  stdbdbl  24836  metcnp3  24859  metcnp2  24861  txmetcnp  24866  blval2  24881  nmoix  25048  nmoeq0  25055  icoopnst  25260  iocopnst  25261  xrhmeo  25267  nmhmcn  25441  cphsqrtcl2  25507  cphsqrtcl3  25508  cfil3i  25590  caublcls  25630  bcthlem5  25649  cmetcusp1  25674  cssbn  25696  rrxcph  25713  pjth  25760  ovoliunlem2  25824  volun  25866  volsup2  25926  mbfimaopn2  25978  iblconst  26138  itgconst  26139  dvcnp2  26240  dvcn  26241  deg1mul3le  26435  deg1tmle  26436  dvdsq1p  26481  ig1peu  26493  ig1pdvds  26498  coeid3  26559  dgrmulc  26590  efcvx  26776  tanord  26866  logdivlti  26948  logccv  26991  recxpcl  27003  cxpeq  27085  ang180  27142  isosctrlem2  27147  cxp2lim  27304  amgm  27318  muval1  27460  dvdssqf  27465  mumullem2  27507  mumul  27508  bcmono  27604  lgsfcl2  27630  lgsdilem  27651  lgsdirprm  27658  lgsdir  27659  lgsdi  27661  lgsne0  27662  padicabv  27957  nosep1o  28038  nosep2o  28039  nosepssdm  28043  nolt02olem  28051  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem4  28068  nosupbnd1lem5  28069  nosupbnd1lem6  28070  nosupbnd2  28073  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem4  28083  noinfbnd1lem6  28085  noinfbnd2  28088  noetasuplem3  28092  noetalem1  28098  cutbdaybnd  28181  ltslpss  28294  leslss  28295  coinitslts  28305  addsass  28391  addsdi  28541  mulsass  28552  norecdiv  28576  bdayfinbndlem1  28853  z12bdaylem  28870  brbtwn2  29483  colinearalglem1  29484  colinearalg  29488  axcgrtr  29493  axsegconlem8  29502  axsegconlem9  29503  axsegconlem10  29504  axcontlem8  29549  axcontlem10  29551  elntg2  29563  vtxdlfuhgr1v  30060  umgr2wlk  30538  erclwwlksym  30612  clwwlkfo  30641  clwwlkext2edg  30647  erclwwlknsym  30661  clwwlknon1  30688  numclwwlk2lem1  30977  numclwwlk5  30989  frgrregord13  30997  nvmul0or  31252  ipval2lem2  31306  lnomul  31362  shless  31961  shlej1  31962  pjspansn  32179  hoadddi  32405  kbmul  32557  homco2  32579  kbass2  32719  eliccelico  33369  elicoelioo  33370  iocinioc2  33371  iocinif  33373  swrdrn2  33517  xrge0adddir  33579  xrge0npcan  33581  archiabl  33759  ress1r  33793  grplsm0l  33954  intlidl  33970  ssmxidl  33999  pstmfval  34528  fmcncfil  34563  zrhnm  34599  qqhnm  34622  measvunilem  34845  volfiniune  34863  dya2iocnrect  34913  sibfinima  34971  probun  35051  probinc  35053  cndprob01  35067  signstfvp  35200  bnj517  35515  bnj594  35542  pconnpi1  36002  cvmsss2  36039  mrsubcv  36275  msubvrs  36325  br6  36522  br4  36523  cgrcomim  36754  cgrtriv  36767  cgrextend  36773  segconeq  36775  btwntriv2  36777  btwnintr  36784  btwnexch3  36785  btwnouttr2  36787  trisegint  36793  cgrsub  36810  cgrxfr  36820  btwnxfr  36821  lineext  36841  btwnconn1lem13  36864  btwnconn1lem14  36865  btwnconn3  36868  segcon2  36870  brsegle  36873  brsegle2  36874  segletr  36879  segleantisym  36880  seglelin  36881  outsideofeu  36896  lineunray  36912  lineelsb2  36913  nmulss1  36963  ltnmul  36965  nmulle  36966  ltnadd  36967  naddle  36968  nadddi  36973  ivthALT  37123  weiunpo  37253  weiunso  37254  weiunfr  37255  weiunse  37256  areacirc  38631  cocanfo  38653  upixp  38663  ismtyima  38737  rrndstprj2  38765  zerdivemp1x  38881  lsatfixedN  40066  lssat  40073  eqlkr  40156  eqlkr2  40157  lkrlsp  40159  lshpkrlem4  40170  opposet  40238  cvrcon3b  40334  cvrcmp  40340  atlen0  40367  atnle  40374  atlatmstc  40376  cvlatexch3  40395  cvlsupr2  40400  hlsupr2  40444  hlrelat2  40460  cvrexchlem  40476  lnnat  40484  atcvrj2b  40489  atle  40493  atexchcvrN  40497  atbtwn  40503  athgt  40513  3dimlem3  40518  3dim1  40524  1cvratlt  40531  1cvrjat  40532  ps-1  40534  ps-2  40535  3atlem3  40542  3atlem5  40544  3atlem7  40546  llni  40565  llni2  40569  atcvrlln2  40576  llnexatN  40578  llncmp  40579  2llnmat  40581  2at0mat0  40582  lplni  40589  lplnnle2at  40598  2atnelpln  40601  lplnllnneN  40613  llncvrlpln2  40614  2lplnmN  40616  2llnmj  40617  lplncmp  40619  lplnexatN  40620  lplnexllnN  40621  2llnm3N  40626  lvoli  40632  lvoli3  40634  islvol2aN  40649  4atlem0a  40650  4atlem3  40653  4atlem3a  40654  4atlem4a  40656  4atlem4b  40657  4atlem4c  40658  4atlem4d  40659  4atlem10b  40662  4atlem11  40666  4atlem12  40669  lplncvrlvol2  40672  lvolcmp  40674  2lplnmj  40679  islinei  40797  pmapglbx  40826  linepmap  40832  lneq2at  40835  lnjatN  40837  lncvrat  40839  lncmp  40840  2llnma3r  40845  elpaddatriN  40860  elpaddat  40861  paddcom  40870  paddss1  40874  paddss2  40875  paddss12  40876  paddasslem6  40882  paddasslem7  40883  paddasslem8  40884  paddasslem9  40885  paddasslem15  40891  pmodlem2  40904  pmodl42N  40908  pmapjoin  40909  llnmod1i2  40917  2polcon4bN  40975  polcon2bN  40977  poml4N  41010  poml6N  41012  osumcllem1N  41013  osumcllem2N  41014  osumcllem11N  41023  osumclN  41024  pmapojoinN  41025  pexmidlem2N  41028  pexmidlem3N  41029  pexmidlem4N  41030  pexmidlem6N  41032  pexmidlem7N  41033  pl42lem2N  41037  pl42lem3N  41038  pl42lem4N  41039  pl42N  41040  lhpexle2lem  41066  lhpexle3lem  41068  lhpexle3  41069  lhpmcvr3  41082  lhp2at0nle  41092  lhprelat3N  41097  4atex  41133  4atex2  41134  lauteq  41152  lautco  41154  ltrncoidN  41185  ltrneq2  41205  ltrnnidn  41231  ltrnideq  41232  trlnid  41236  ltrnatlw  41240  trlnle  41243  trlval3  41244  trlval4  41245  cdlemc  41254  cdlemd5  41259  cdlemd9  41263  ltrneq3  41265  cdleme0moN  41282  cdleme20  41381  cdleme21j  41393  cdleme21  41394  cdleme27cl  41423  cdlemefrs29bpre0  41453  cdlemefs27cl  41470  cdlemefs32sn1aw  41471  cdleme43fsv1snlem  41477  cdleme32d  41501  cdleme32f  41503  cdleme32le  41504  cdleme35h2  41514  cdleme38n  41521  cdleme40m  41524  cdleme41snaw  41533  cdleme42ke  41542  cdleme17d3  41553  cdleme48fvg  41557  cdlemeg46fvcl  41563  cdlemeg46fgN  41591  cdleme48gfv1  41593  cdleme48fgv  41595  cdleme50trn3  41610  trlord  41626  ltrniotavalbN  41641  cdlemb3  41663  cdlemg6c  41677  cdlemg6  41680  cdlemg7N  41683  cdlemg8c  41686  cdlemg8  41688  cdlemg11a  41694  cdlemg11b  41699  cdlemg12e  41704  cdlemg15a  41712  cdlemg15  41713  cdlemg16  41714  cdlemg16z  41716  cdlemg16zz  41717  cdlemg17dN  41720  cdlemg18a  41735  cdlemg20  41742  cdlemg22  41744  cdlemg24  41745  cdlemg37  41746  cdlemg31d  41757  cdlemg29  41762  cdlemg33b  41764  cdlemg33  41768  cdlemg38  41772  cdlemg39  41773  cdlemg40  41774  trlco  41784  trlcone  41785  cdlemg42  41786  cdlemg44b  41789  ltrncom  41795  trljco  41797  tendococl  41829  tendoplcl  41838  tendoplcom  41839  cdlemj2  41879  cdlemj3  41880  tendoid0  41882  tendoconid  41886  tendotr  41887  cdlemk25-3  41961  cdlemk26b-3  41962  cdlemk34  41967  cdlemk36  41970  cdlemk38  41972  cdlemkid4  41991  cdlemk35s-id  41995  cdlemk39s-id  41997  cdlemk19x  42000  cdlemk53  42014  cdlemk55  42018  cdlemk55u  42023  cdlemk39u  42025  cdlemk19u  42027  cdlemk56  42028  tendoex  42032  cdleml3N  42035  cdleml5N  42037  tendospcanN  42080  cdlemm10N  42175  cdlemn11pre  42267  dihord2pre  42282  dihvalcqpre  42292  dihopelvalcpre  42305  dihord6apre  42313  dihord5b  42316  dihord5apre  42319  dihord  42321  dihmeetlem1N  42347  dihglblem5apreN  42348  dihglblem3N  42352  dihmeetlem2N  42356  dihglbcpreN  42357  dihmeetbN  42360  dihmeetlem4preN  42363  dihmeetlem5  42365  dihmeetlem7N  42367  dihmeetlem10N  42373  dihmeetlem11N  42374  dihmeetlem12N  42375  dihmeetlem13N  42376  dihmeetlem15N  42378  dihmeetlem16N  42379  dihmeetlem17N  42380  dihmeetlem18N  42381  dihmeetlem19N  42382  dihmeetALTN  42384  dih1dimatlem0  42385  dihlspsnssN  42389  dihlspsnat  42390  mapdh8ad  42836  hdmap14lem14  42938  hgmapvvlem3  42982  aks6d1c6isolem1  43224  resubcan2  43439  mzprename  43759  eldioph2lem1  43770  lzunuz  43778  rencldnfi  43827  pellexlem2  43836  infmrgelbi  43884  pellfundglb  43891  pellfund14gap  43893  qirropth  43914  rmxycomplete  43923  congadd  43972  acongeq  43989  jm2.19  43999  jm2.23  44002  jm2.20nn  44003  jm2.27  44014  jm3.1  44026  aomclem6  44060  lnmepi  44086  lmhmfgsplit  44087  lmhmlnmsplit  44088  pwssplit4  44090  hbtlem2  44125  hbtlem5  44129  dgraa0p  44150  proot1hash  44196  iocunico  44212  oasubex  44287  oege1  44307  relexpxpmin  44716  brtrclfv2  44726  ntrclsiso  45066  ntrclskb  45068  ntrclsk3  45069  k0004lem3  45148  grur1cld  45229  ismnu  45244  grumnudlem  45268  suprnmpt  46188  wessf1ornlem  46199  projf1o  46210  snunioo1  46523  iccintsng  46534  lptre2pt  46649  limcleqr  46653  fnlimfvre  46683  limsupgtlem  46786  volioc  46981  iblspltprt  46982  stoweidlem19  47028  stoweidlem20  47029  stoweidlem22  47031  stoweidlem28  47037  stoweidlem34  47043  stoweidlem44  47053  stoweidlem60  47069  wallispilem3  47076  fourierdlem41  47157  fourierdlem42  47158  fourierdlem49  47164  fourierdlem51  47166  fourierdlem54  47169  fourierdlem74  47189  fourierdlem97  47212  caratheodorylem2  47536  ovnsubaddlem2  47580  hspmbllem2  47636  smflimmpt  47819  smflimsupmpt  47838  smfliminfmpt  47841  funfocofob  48147  fzopredsuc  48393  nnmul2b  48400  imasetpreimafvbijlemfv  48483  iccpartigtl  48504  lighneal  48695  oexpnegALTV  48774  oexpnegnz  48775  tgblthelfgott  48912  clnbgrgrim  49031  uhgrimgrlim  49084  gpgusgralem  49153  lidldomn1  49327  ofaddmndmap  49454  lincdifsn  49535  lincellss  49537  lincresunit3lem3  49585  islindeps2  49594  lindssnlvec  49597  fdivmptf  49652  refdivmptf  49653  rrx2linest  49853  itsclc0yqsollem1  49873  itsclc0b  49883  itsclquadb  49887  itscnhlinecirc02plem3  49895  diag1  50411  setc1onsubc  50709