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  3594  2nreu  4394  predtrss  6269  frpomin  6287  f1prex  7218  cocan1  7225  weniso  7288  frrlem4  8219  frrlem10  8225  fprlem1  8230  smogt  8287  smocdmdom  8288  omeulem1  8497  nnmord  8547  nnmword  8548  naddasslem1  8609  naddasslem2  8610  difsnen  8972  enfixsn  8999  mapunen  9059  ac6sfi  9168  fipreima  9242  elfiun  9314  ordiso2  9401  wemaplem2  9433  en2eqpr  9895  indcardi  9929  fodomfi2  9948  iunfictbso  10002  infmap2  10105  cofsmo  10157  cfsmolem  10158  coftr  10161  fin23lem11  10205  fincssdom  10211  fin23lem26  10213  isf32lem9  10249  ac6num  10367  gchdomtri  10517  gchpwdom  10558  winainflem  10581  tskuni  10671  gruima  10690  gruf  10699  grudomon  10705  elnpi  10876  distrlem4pr  10914  prlem934  10921  addcan  11294  addcan2  11295  divmulass  11796  divmulasscom  11797  ltmul1a  11967  suprleub  12085  supmul1  12088  suprzcl  12550  uzsupss  12835  xleadd1a  13149  xlesubadd  13159  xmulasslem3  13182  xlemul2a  13185  xadddilem  13190  xadddi2  13193  ixxun  13258  icoshftf1o  13371  ioounsn  13374  snunioc  13377  lincmb01cmp  13392  iccf1o  13393  nn0p1elfzo  13599  fzofzim  13606  fzoopth  13659  ltexp2a  14070  leexp2  14075  ltexp2r  14077  exple1  14081  expnlbnd2  14138  fun2dmnop0  14408  ccatass  14493  swrdswrdlem  14608  ccatopth  14620  repswpfx  14689  2cshw  14717  cshimadifsn  14733  cshimadifsn0  14734  cshco  14740  repsco  14744  s2f1o  14820  limsupgre  15385  addcn2  15498  mulcn2  15500  ntrivcvgmul  15806  binomrisefac  15946  dvdsmodexp  16168  dvdsadd2b  16214  dvdsexp2im  16235  dvdsmod  16237  oexpneg  16253  sadass  16379  gcdass  16455  rplpwr  16466  lcmfunsnlem1  16545  coprmdvds2  16562  rpmulgcd2  16564  qredeq  16565  rpdvds  16568  cncongr2  16576  rpexp  16630  prmdiveq  16694  hashgcdlem  16696  odzdvds  16704  modprmn0modprm0  16716  coprimeprodsq2  16718  pythagtriplem3  16727  pcdvdsb  16778  pcgcd1  16786  qexpz  16810  pockthg  16815  vdwnnlem1  16904  0ram  16929  ramz2  16933  lubss  18416  lubun  18418  clatleglb  18421  clatglbss  18422  mrelatglb  18463  isnsgrp  18628  issubmnd  18666  ress0g  18667  mhmvlin  18706  gsumccat  18746  frmdss2  18768  submefmnd  18800  mulgneg  19002  mulgdirlem  19015  submmulg  19028  subgmulg  19050  nmzsubg  19075  ghmmulg  19138  gsmsymgreqlem1  19340  pmtrfb  19375  psgnunilem4  19407  odmodnn0  19450  odnncl  19455  odmod  19456  odmulgid  19464  odmulgeq  19467  odf1o1  19482  odf1o2  19483  odngen  19487  gexdvdsi  19493  pgpfi1  19505  odcau  19514  subgslw  19526  fislw  19535  lsmssv  19553  lsmless1x  19554  lsmless2x  19555  lsmsubm  19563  lsmmod  19585  lsmmod2  19586  efgred  19658  cntzcmn  19750  ghmplusg  19756  odadd1  19758  odadd2  19759  odadd  19760  lsmcomx  19766  gsumconst  19844  ablsimpgprmd  20027  srg1zr  20131  ring1eq0  20214  mulgass2  20225  rngisom1  20382  rhmdvdsr  20421  isabvd  20725  rmodislmodlem  20860  rmodislmod  20861  lssintcl  20895  0lmhm  20972  lmhmvsca  20977  reslmhm2b  20986  pwssplit1  20991  pwssplit3  20993  lspfixed  21063  lspsnat  21080  rnglidlrng  21182  2idlcpblrng  21206  lidldvgen  21269  xrsdsreclblem  21347  regsumsupp  21557  obselocv  21663  uvcresum  21728  frlmsslsp  21731  frlmup4  21736  lindff1  21755  f1lindf  21757  lsslindf  21765  islindf4  21773  lbslcic  21776  issubassa  21802  evlsval2  22020  psrplusgpropd  22146  coe1subfv  22178  coe1mul2  22181  mpomatmul  22359  mamutpos  22371  scmatscmide  22420  mavmulsolcl  22464  marrepcl  22477  mdetdiag  22512  mdetunilem1  22525  mdetunilem3  22527  mdetunilem7  22531  mdetunilem9  22533  mdetmul  22536  slesolinvbi  22594  m2pmfzmap  22660  pmatcollpwlem  22693  pmatcollpw  22694  mp2pm2mplem4  22722  chpdmatlem3  22753  chfacfisfcpmat  22768  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  chfacfpmmulgsum2  22778  cayhamlem1  22779  cpmidpmatlem2  22784  cpmadugsumlemB  22787  cpmadugsumlemC  22788  cpmadugsumlemF  22789  riinopn  22821  neiint  23017  topssnei  23037  restntr  23095  iscnp4  23176  cnconst2  23196  cnrest2  23199  cnprest2  23203  cnpdis  23206  cnt0  23259  cnt1  23263  cnhaus  23267  ordthauslem  23296  cncmp  23305  fiuncmp  23317  sscmp  23318  hauscmp  23320  cnconn  23335  unconn  23342  nlly2i  23389  llynlly  23390  nllyidm  23402  finlocfin  23433  ptrescn  23552  xkococnlem  23572  qtopss  23628  kqfvima  23643  r0cld  23651  ordthmeolem  23714  fbssint  23751  fmf  23858  fmss  23859  elfm  23860  rnelfmlem  23865  rnelfm  23866  fmco  23874  flimss2  23885  flimss1  23886  flimrest  23896  flftg  23909  cnpflf2  23913  cnpflf  23914  flfcnp  23917  supnfcls  23933  fclsss1  23935  fclsss2  23936  fcfnei  23948  fcfelbas  23949  cnpfcfi  23953  subgntr  24020  opnsubg  24021  cldsubg  24024  ghmcnp  24028  utop2nei  24163  neipcfilu  24208  bldisj  24311  blgt0  24312  bl2in  24313  blss2ps  24316  blss2  24317  blssps  24337  blss  24338  xmetresbl  24350  lpbl  24416  blcld  24418  stdbdbl  24430  metcnp3  24453  metcnp2  24455  txmetcnp  24460  blval2  24475  nmoix  24642  nmoeq0  24649  icoopnst  24861  iocopnst  24862  xrhmeo  24869  nmhmcn  25045  cphsqrtcl2  25111  cphsqrtcl3  25112  cfil3i  25194  caublcls  25234  bcthlem5  25253  cmetcusp1  25278  cssbn  25300  rrxcph  25317  pjth  25364  ovoliunlem2  25429  volun  25471  volsup2  25531  mbfimaopn2  25583  iblconst  25744  itgconst  25745  dvcnp2  25846  dvcnp2OLD  25847  dvcn  25848  deg1mul3le  26047  deg1tmle  26048  dvdsq1p  26093  ig1peu  26105  ig1pdvds  26110  coeid3  26170  dgrmulc  26202  efcvx  26384  tanord  26472  logdivlti  26554  logccv  26597  recxpcl  26609  cxpeq  26692  ang180  26749  isosctrlem2  26754  cxp2lim  26912  amgm  26926  muval1  27068  dvdssqf  27073  mumullem2  27115  mumul  27116  bcmono  27213  lgsfcl2  27239  lgsdilem  27260  lgsdirprm  27267  lgsdir  27268  lgsdi  27270  lgsne0  27271  padicabv  27566  nosep1o  27618  nosep2o  27619  nosepssdm  27623  nolt02olem  27631  nosupres  27644  nosupbnd1lem1  27645  nosupbnd1lem4  27648  nosupbnd1lem5  27649  nosupbnd1lem6  27650  nosupbnd2  27653  noinfres  27659  noinfbnd1lem1  27660  noinfbnd1lem4  27663  noinfbnd1lem6  27665  noinfbnd2  27668  noetasuplem3  27672  noetalem1  27678  scutbdaybnd  27754  sltlpss  27851  slelss  27852  coinitsslt  27861  addsass  27946  addsdi  28092  mulsass  28103  norecdiv  28127  brbtwn2  28881  colinearalglem1  28882  colinearalg  28886  axcgrtr  28891  axsegconlem8  28900  axsegconlem9  28901  axsegconlem10  28902  axcontlem8  28947  axcontlem10  28949  elntg2  28961  vtxdlfuhgr1v  29456  umgr2wlk  29925  erclwwlksym  29996  clwwlkfo  30025  clwwlkext2edg  30031  erclwwlknsym  30045  clwwlknon1  30072  numclwwlk2lem1  30351  numclwwlk5  30363  frgrregord13  30371  nvmul0or  30625  ipval2lem2  30679  lnomul  30735  shless  31334  shlej1  31335  pjspansn  31552  hoadddi  31778  kbmul  31930  homco2  31952  kbass2  32092  eliccelico  32755  elicoelioo  32756  iocinioc2  32757  iocinif  32759  swrdrn2  32930  xrge0adddir  32994  xrge0npcan  32996  archiabl  33162  ress1r  33196  pidlnz  33336  grplsm0l  33363  intlidl  33380  ssmxidl  33434  pstmfval  33904  fmcncfil  33939  zrhnm  33975  qqhnm  33998  measvunilem  34220  volfiniune  34238  dya2iocnrect  34289  sibfinima  34347  probun  34427  probinc  34429  cndprob01  34443  signstfvp  34579  bnj517  34892  bnj594  34919  fissorduni  35096  pconnpi1  35269  cvmsss2  35306  mrsubcv  35542  msubvrs  35592  br6  35789  br4  35790  cgrcomim  36022  cgrtriv  36035  cgrextend  36041  segconeq  36043  btwntriv2  36045  btwnintr  36052  btwnexch3  36053  btwnouttr2  36055  trisegint  36061  cgrsub  36078  cgrxfr  36088  btwnxfr  36089  lineext  36109  btwnconn1lem13  36132  btwnconn1lem14  36133  btwnconn3  36136  segcon2  36138  brsegle  36141  brsegle2  36142  segletr  36147  segleantisym  36148  seglelin  36149  outsideofeu  36164  lineunray  36180  lineelsb2  36181  ivthALT  36368  weiunpo  36498  weiunso  36499  weiunfr  36500  weiunse  36501  lindsenlbs  37654  areacirc  37752  cocanfo  37758  upixp  37768  ismtyima  37842  rrndstprj2  37870  zerdivemp1x  37986  lsatfixedN  39047  lssat  39054  eqlkr  39137  eqlkr2  39138  lkrlsp  39140  lshpkrlem4  39151  opposet  39219  cvrcon3b  39315  cvrcmp  39321  atlen0  39348  atnle  39355  atlatmstc  39357  cvlatexch3  39376  cvlsupr2  39381  hlsupr2  39425  hlrelat2  39441  cvrexchlem  39457  lnnat  39465  atcvrj2b  39470  atle  39474  atexchcvrN  39478  atbtwn  39484  athgt  39494  3dimlem3  39499  3dim1  39505  1cvratlt  39512  1cvrjat  39513  ps-1  39515  ps-2  39516  3atlem3  39523  3atlem5  39525  3atlem7  39527  llni  39546  llni2  39550  atcvrlln2  39557  llnexatN  39559  llncmp  39560  2llnmat  39562  2at0mat0  39563  lplni  39570  lplnnle2at  39579  2atnelpln  39582  lplnllnneN  39594  llncvrlpln2  39595  2lplnmN  39597  2llnmj  39598  lplncmp  39600  lplnexatN  39601  lplnexllnN  39602  2llnm3N  39607  lvoli  39613  lvoli3  39615  islvol2aN  39630  4atlem0a  39631  4atlem3  39634  4atlem3a  39635  4atlem4a  39637  4atlem4b  39638  4atlem4c  39639  4atlem4d  39640  4atlem10b  39643  4atlem11  39647  4atlem12  39650  lplncvrlvol2  39653  lvolcmp  39655  2lplnmj  39660  islinei  39778  pmapglbx  39807  linepmap  39813  lneq2at  39816  lnjatN  39818  lncvrat  39820  lncmp  39821  2llnma3r  39826  elpaddatriN  39841  elpaddat  39842  paddcom  39851  paddss1  39855  paddss2  39856  paddss12  39857  paddasslem6  39863  paddasslem7  39864  paddasslem8  39865  paddasslem9  39866  paddasslem15  39872  pmodlem2  39885  pmodl42N  39889  pmapjoin  39890  llnmod1i2  39898  2polcon4bN  39956  polcon2bN  39958  poml4N  39991  poml6N  39993  osumcllem1N  39994  osumcllem2N  39995  osumcllem11N  40004  osumclN  40005  pmapojoinN  40006  pexmidlem2N  40009  pexmidlem3N  40010  pexmidlem4N  40011  pexmidlem6N  40013  pexmidlem7N  40014  pl42lem2N  40018  pl42lem3N  40019  pl42lem4N  40020  pl42N  40021  lhpexle2lem  40047  lhpexle3lem  40049  lhpexle3  40050  lhpmcvr3  40063  lhp2at0nle  40073  lhprelat3N  40078  4atex  40114  4atex2  40115  lauteq  40133  lautco  40135  ltrncoidN  40166  ltrneq2  40186  ltrnnidn  40212  ltrnideq  40213  trlnid  40217  ltrnatlw  40221  trlnle  40224  trlval3  40225  trlval4  40226  cdlemc  40235  cdlemd5  40240  cdlemd9  40244  ltrneq3  40246  cdleme0moN  40263  cdleme20  40362  cdleme21j  40374  cdleme21  40375  cdleme27cl  40404  cdlemefrs29bpre0  40434  cdlemefs27cl  40451  cdlemefs32sn1aw  40452  cdleme43fsv1snlem  40458  cdleme32d  40482  cdleme32f  40484  cdleme32le  40485  cdleme35h2  40495  cdleme38n  40502  cdleme40m  40505  cdleme41snaw  40514  cdleme42ke  40523  cdleme17d3  40534  cdleme48fvg  40538  cdlemeg46fvcl  40544  cdlemeg46fgN  40572  cdleme48gfv1  40574  cdleme48fgv  40576  cdleme50trn3  40591  trlord  40607  ltrniotavalbN  40622  cdlemb3  40644  cdlemg6c  40658  cdlemg6  40661  cdlemg7N  40664  cdlemg8c  40667  cdlemg8  40669  cdlemg11a  40675  cdlemg11b  40680  cdlemg12e  40685  cdlemg15a  40693  cdlemg15  40694  cdlemg16  40695  cdlemg16z  40697  cdlemg16zz  40698  cdlemg17dN  40701  cdlemg18a  40716  cdlemg20  40723  cdlemg22  40725  cdlemg24  40726  cdlemg37  40727  cdlemg31d  40738  cdlemg29  40743  cdlemg33b  40745  cdlemg33  40749  cdlemg38  40753  cdlemg39  40754  cdlemg40  40755  trlco  40765  trlcone  40766  cdlemg42  40767  cdlemg44b  40770  ltrncom  40776  trljco  40778  tendococl  40810  tendoplcl  40819  tendoplcom  40820  cdlemj2  40860  cdlemj3  40861  tendoid0  40863  tendoconid  40867  tendotr  40868  cdlemk25-3  40942  cdlemk26b-3  40943  cdlemk34  40948  cdlemk36  40951  cdlemk38  40953  cdlemkid4  40972  cdlemk35s-id  40976  cdlemk39s-id  40978  cdlemk19x  40981  cdlemk53  40995  cdlemk55  40999  cdlemk55u  41004  cdlemk39u  41006  cdlemk19u  41008  cdlemk56  41009  tendoex  41013  cdleml3N  41016  cdleml5N  41018  tendospcanN  41061  cdlemm10N  41156  cdlemn11pre  41248  dihord2pre  41263  dihvalcqpre  41273  dihopelvalcpre  41286  dihord6apre  41294  dihord5b  41297  dihord5apre  41300  dihord  41302  dihmeetlem1N  41328  dihglblem5apreN  41329  dihglblem3N  41333  dihmeetlem2N  41337  dihglbcpreN  41338  dihmeetbN  41341  dihmeetlem4preN  41344  dihmeetlem5  41346  dihmeetlem7N  41348  dihmeetlem10N  41354  dihmeetlem11N  41355  dihmeetlem12N  41356  dihmeetlem13N  41357  dihmeetlem15N  41359  dihmeetlem16N  41360  dihmeetlem17N  41361  dihmeetlem18N  41362  dihmeetlem19N  41363  dihmeetALTN  41365  dih1dimatlem0  41366  dihlspsnssN  41370  dihlspsnat  41371  mapdh8ad  41817  hdmap14lem14  41919  hgmapvvlem3  41963  aks6d1c6isolem1  42206  dvdsexpnn  42365  resubcan2  42420  mzprename  42781  eldioph2lem1  42792  lzunuz  42800  rencldnfi  42853  pellexlem2  42862  infmrgelbi  42910  pellfundglb  42917  pellfund14gap  42919  qirropth  42940  rmxycomplete  42949  congadd  42998  acongeq  43015  jm2.19  43025  jm2.23  43028  jm2.20nn  43029  jm2.27  43040  jm3.1  43052  aomclem6  43091  lnmepi  43117  lmhmfgsplit  43118  lmhmlnmsplit  43119  pwssplit4  43121  hbtlem2  43156  hbtlem5  43160  dgraa0p  43181  proot1hash  43227  iocunico  43243  oasubex  43318  oege1  43338  relexpxpmin  43749  brtrclfv2  43759  ntrclsiso  44099  ntrclskb  44101  ntrclsk3  44102  k0004lem3  44181  grur1cld  44264  ismnu  44293  grumnudlem  44317  suprnmpt  45210  wessf1ornlem  45221  projf1o  45233  snunioo1  45551  iccintsng  45562  lptre2pt  45677  limcleqr  45681  fnlimfvre  45711  limsupgtlem  45814  volioc  46009  iblspltprt  46010  stoweidlem19  46056  stoweidlem20  46057  stoweidlem22  46059  stoweidlem28  46065  stoweidlem34  46071  stoweidlem44  46081  stoweidlem60  46097  wallispilem3  46104  fourierdlem41  46185  fourierdlem42  46186  fourierdlem49  46192  fourierdlem51  46194  fourierdlem54  46197  fourierdlem74  46217  fourierdlem97  46240  caratheodorylem2  46564  ovnsubaddlem2  46608  hspmbllem2  46664  smflimmpt  46847  smflimsupmpt  46866  smfliminfmpt  46869  funfocofob  47108  fzopredsuc  47353  imasetpreimafvbijlemfv  47432  iccpartigtl  47453  lighneal  47641  oexpnegALTV  47707  oexpnegnz  47708  tgblthelfgott  47845  clnbgrgrim  47964  uhgrimgrlim  48017  gpgusgralem  48086  lidldomn1  48261  ofaddmndmap  48373  lincdifsn  48455  lincellss  48457  lincresunit3lem3  48505  islindeps2  48514  lindssnlvec  48517  fdivmptf  48572  refdivmptf  48573  rrx2linest  48773  itsclc0yqsollem1  48793  itsclc0b  48803  itsclquadb  48807  itscnhlinecirc02plem3  48815  diag1  49335  setc1onsubc  49633