Theorem simpl1 1188

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  simpl11  1245  simpl21  1248  simpl31  1251  simp1l1  1263  simp2l1  1269  simp3l1  1275  3anandirs  1468  rspc3ev  3628  2nreu  4445  predtrss  6333  frpomin  6351  f1prex  7299  cocan1  7306  weniso  7368  frrlem4  8301  frrlem10  8307  fprlem1  8312  smogt  8394  smocdmdom  8395  omeulem1  8609  nnmord  8659  nnmword  8660  naddasslem1  8721  naddasslem2  8722  difsnen  9084  enfixsn  9112  mapunen  9177  ac6sfi  9318  fipreima  9390  elfiun  9461  ordiso2  9546  wemaplem2  9578  en2eqpr  10038  indcardi  10072  fodomfi2  10091  iunfictbso  10145  infmap2  10249  cofsmo  10300  cfsmolem  10301  coftr  10304  fin23lem11  10348  fincssdom  10354  fin23lem26  10356  isf32lem9  10392  ac6num  10510  gchdomtri  10660  gchpwdom  10701  winainflem  10724  tskuni  10814  gruima  10833  gruf  10842  grudomon  10848  elnpi  11019  distrlem4pr  11057  prlem934  11064  addcan  11436  addcan2  11437  divmulass  11933  divmulasscom  11934  ltmul1a  12101  suprleub  12218  supmul1  12221  suprzcl  12680  uzsupss  12962  xleadd1a  13272  xlesubadd  13282  xmulasslem3  13305  xlemul2a  13308  xadddilem  13313  xadddi2  13316  ixxun  13380  icoshftf1o  13491  ioounsn  13494  snunioc  13497  lincmb01cmp  13512  iccf1o  13513  nn0p1elfzo  13715  fzofzim  13719  ltexp2a  14170  leexp2  14175  ltexp2r  14177  exple1  14180  expnlbnd2  14236  fun2dmnop0  14495  ccatass  14578  swrdswrdlem  14694  ccatopth  14706  repswpfx  14775  2cshw  14803  cshimadifsn  14820  cshimadifsn0  14821  cshco  14827  repsco  14831  s2f1o  14907  limsupgre  15465  addcn2  15578  mulcn2  15580  ntrivcvgmul  15888  binomrisefac  16026  dvdsmodexp  16246  dvdsadd2b  16290  dvdsexp2im  16311  dvdsmod  16313  oexpneg  16329  sadass  16453  gcdass  16530  rplpwr  16540  lcmfunsnlem1  16615  coprmdvds2  16632  rpmulgcd2  16634  qredeq  16635  rpdvds  16638  cncongr2  16646  rpexp  16701  prmdiveq  16762  hashgcdlem  16764  odzdvds  16771  modprmn0modprm0  16783  coprimeprodsq2  16785  pythagtriplem3  16794  pcdvdsb  16845  pcgcd1  16853  qexpz  16877  pockthg  16882  vdwnnlem1  16971  0ram  16996  ramz2  17000  lubss  18512  lubun  18514  clatleglb  18517  clatglbss  18518  mrelatglb  18559  isnsgrp  18690  issubmnd  18728  ress0g  18729  gsumccat  18800  frmdss2  18822  submefmnd  18854  mulgneg  19054  mulgdirlem  19067  submmulg  19080  subgmulg  19102  nmzsubg  19127  ghmmulg  19189  gsmsymgreqlem1  19392  pmtrfb  19427  psgnunilem4  19459  odmodnn0  19502  odnncl  19507  odmod  19508  odmulgid  19516  odmulgeq  19519  odf1o1  19534  odf1o2  19535  odngen  19539  gexdvdsi  19545  pgpfi1  19557  odcau  19566  subgslw  19578  fislw  19587  lsmssv  19605  lsmless1x  19606  lsmless2x  19607  lsmsubm  19615  lsmmod  19637  lsmmod2  19638  efgred  19710  cntzcmn  19802  ghmplusg  19808  odadd1  19810  odadd2  19811  odadd  19812  lsmcomx  19818  gsumconst  19896  ablsimpgprmd  20079  srg1zr  20162  ring1eq0  20241  mulgass2  20252  rngisom1  20412  rhmdvdsr  20454  isabvd  20707  rmodislmodlem  20819  rmodislmod  20820  rmodislmodOLD  20821  lssintcl  20855  0lmhm  20932  lmhmvsca  20937  reslmhm2b  20946  pwssplit1  20951  pwssplit3  20953  lspfixed  21023  lspsnat  21040  rnglidlrng  21149  2idlcpblrng  21172  lidldvgen  21231  xrsdsreclblem  21352  regsumsupp  21561  obselocv  21669  uvcresum  21734  frlmsslsp  21737  frlmup4  21742  lindff1  21761  f1lindf  21763  lsslindf  21771  islindf4  21779  lbslcic  21782  issubassa  21807  evlsval2  22040  psrplusgpropd  22161  coe1subfv  22192  coe1mul2  22195  mhmvlin  22319  mpomatmul  22368  mamutpos  22380  scmatscmide  22429  mavmulsolcl  22473  marrepcl  22486  mdetdiag  22521  mdetunilem1  22534  mdetunilem3  22536  mdetunilem7  22540  mdetunilem9  22542  mdetmul  22545  slesolinvbi  22603  m2pmfzmap  22669  pmatcollpwlem  22702  pmatcollpw  22703  mp2pm2mplem4  22731  chpdmatlem3  22762  chfacfisfcpmat  22777  chfacfscmulgsum  22782  chfacfpmmulgsum  22786  chfacfpmmulgsum2  22787  cayhamlem1  22788  cpmidpmatlem2  22793  cpmadugsumlemB  22796  cpmadugsumlemC  22797  cpmadugsumlemF  22798  riinopn  22830  neiint  23028  topssnei  23048  restntr  23106  iscnp4  23187  cnconst2  23207  cnrest2  23210  cnprest2  23214  cnpdis  23217  cnt0  23270  cnt1  23274  cnhaus  23278  ordthauslem  23307  cncmp  23316  fiuncmp  23328  sscmp  23329  hauscmp  23331  cnconn  23346  unconn  23353  nlly2i  23400  llynlly  23401  nllyidm  23413  finlocfin  23444  ptrescn  23563  xkococnlem  23583  qtopss  23639  kqfvima  23654  r0cld  23662  ordthmeolem  23725  fbssint  23762  fmf  23869  fmss  23870  elfm  23871  rnelfmlem  23876  rnelfm  23877  fmco  23885  flimss2  23896  flimss1  23897  flimrest  23907  flftg  23920  cnpflf2  23924  cnpflf  23925  flfcnp  23928  supnfcls  23944  fclsss1  23946  fclsss2  23947  fcfnei  23959  fcfelbas  23960  cnpfcfi  23964  subgntr  24031  opnsubg  24032  cldsubg  24035  ghmcnp  24039  utop2nei  24175  neipcfilu  24221  bldisj  24324  blgt0  24325  bl2in  24326  blss2ps  24329  blss2  24330  blssps  24350  blss  24351  xmetresbl  24363  lpbl  24432  blcld  24434  stdbdbl  24446  metcnp3  24469  metcnp2  24471  txmetcnp  24476  blval2  24491  nmoix  24666  nmoeq0  24673  icoopnst  24883  iocopnst  24884  xrhmeo  24891  nmhmcn  25067  cphsqrtcl2  25134  cphsqrtcl3  25135  cfil3i  25217  caublcls  25257  bcthlem5  25276  cmetcusp1  25301  cssbn  25323  rrxcph  25340  pjth  25387  ovoliunlem2  25452  volun  25494  volsup2  25554  mbfimaopn2  25606  iblconst  25767  itgconst  25768  dvcnp2  25869  dvcnp2OLD  25870  dvcn  25871  deg1mul3le  26072  deg1tmle  26073  dvdsq1p  26117  ig1peu  26129  ig1pdvds  26134  coeid3  26194  dgrmulc  26226  efcvx  26406  tanord  26492  logdivlti  26574  logccv  26617  recxpcl  26629  cxpeq  26712  ang180  26766  isosctrlem2  26771  cxp2lim  26929  amgm  26943  muval1  27085  dvdssqf  27090  mumullem2  27132  mumul  27133  bcmono  27230  lgsfcl2  27256  lgsdilem  27277  lgsdirprm  27284  lgsdir  27285  lgsdi  27287  lgsne0  27288  padicabv  27583  nosep1o  27634  nosep2o  27635  nosepssdm  27639  nolt02olem  27647  nosupres  27660  nosupbnd1lem1  27661  nosupbnd1lem4  27664  nosupbnd1lem5  27665  nosupbnd1lem6  27666  nosupbnd2  27669  noinfres  27675  noinfbnd1lem1  27676  noinfbnd1lem4  27679  noinfbnd1lem6  27681  noinfbnd2  27684  noetasuplem3  27688  noetalem1  27694  scutbdaybnd  27768  sltlpss  27853  slelss  27854  coinitsslt  27859  addsass  27942  addsdi  28075  mulsass  28086  norecdiv  28110  brbtwn2  28736  colinearalglem1  28737  colinearalg  28741  axcgrtr  28746  axsegconlem8  28755  axsegconlem9  28756  axsegconlem10  28757  axcontlem8  28802  axcontlem10  28804  elntg2  28816  vtxdlfuhgr1v  29313  umgr2wlk  29780  erclwwlksym  29851  clwwlkfo  29880  clwwlkext2edg  29886  erclwwlknsym  29900  clwwlknon1  29927  numclwwlk2lem1  30206  numclwwlk5  30218  frgrregord13  30226  nvmul0or  30480  ipval2lem2  30534  lnomul  30590  shless  31189  shlej1  31190  pjspansn  31407  hoadddi  31633  kbmul  31785  homco2  31807  kbass2  31947  eliccelico  32566  elicoelioo  32567  iocinioc2  32568  iocinif  32570  swrdrn2  32696  xrge0adddir  32769  xrge0npcan  32771  archiabl  32927  ress1r  32962  pidlnz  33112  grplsm0l  33137  intlidl  33157  ssmxidl  33212  pstmfval  33530  fmcncfil  33565  zrhnm  33603  qqhnm  33624  measvunilem  33864  volfiniune  33882  dya2iocnrect  33934  sibfinima  33992  probun  34072  probinc  34074  cndprob01  34088  signstfvp  34236  bnj517  34549  bnj594  34576  pconnpi1  34880  cvmsss2  34917  mrsubcv  35153  msubvrs  35203  br6  35384  br4  35385  cgrcomim  35618  cgrtriv  35631  cgrextend  35637  segconeq  35639  btwntriv2  35641  btwnintr  35648  btwnexch3  35649  btwnouttr2  35651  trisegint  35657  cgrsub  35674  cgrxfr  35684  btwnxfr  35685  lineext  35705  btwnconn1lem13  35728  btwnconn1lem14  35729  btwnconn3  35732  segcon2  35734  brsegle  35737  brsegle2  35738  segletr  35743  segleantisym  35744  seglelin  35745  outsideofeu  35760  lineunray  35776  lineelsb2  35777  ivthALT  35852  lindsenlbs  37121  areacirc  37219  cocanfo  37225  upixp  37235  ismtyima  37309  rrndstprj2  37337  zerdivemp1x  37453  lsatfixedN  38513  lssat  38520  eqlkr  38603  eqlkr2  38604  lkrlsp  38606  lshpkrlem4  38617  opposet  38685  cvrcon3b  38781  cvrcmp  38787  atlen0  38814  atnle  38821  atlatmstc  38823  cvlatexch3  38842  cvlsupr2  38847  hlsupr2  38892  hlrelat2  38908  cvrexchlem  38924  lnnat  38932  atcvrj2b  38937  atle  38941  atexchcvrN  38945  atbtwn  38951  athgt  38961  3dimlem3  38966  3dim1  38972  1cvratlt  38979  1cvrjat  38980  ps-1  38982  ps-2  38983  3atlem3  38990  3atlem5  38992  3atlem7  38994  llni  39013  llni2  39017  atcvrlln2  39024  llnexatN  39026  llncmp  39027  2llnmat  39029  2at0mat0  39030  lplni  39037  lplnnle2at  39046  2atnelpln  39049  lplnllnneN  39061  llncvrlpln2  39062  2lplnmN  39064  2llnmj  39065  lplncmp  39067  lplnexatN  39068  lplnexllnN  39069  2llnm3N  39074  lvoli  39080  lvoli3  39082  islvol2aN  39097  4atlem0a  39098  4atlem3  39101  4atlem3a  39102  4atlem4a  39104  4atlem4b  39105  4atlem4c  39106  4atlem4d  39107  4atlem10b  39110  4atlem11  39114  4atlem12  39117  lplncvrlvol2  39120  lvolcmp  39122  2lplnmj  39127  islinei  39245  pmapglbx  39274  linepmap  39280  lneq2at  39283  lnjatN  39285  lncvrat  39287  lncmp  39288  2llnma3r  39293  elpaddatriN  39308  elpaddat  39309  paddcom  39318  paddss1  39322  paddss2  39323  paddss12  39324  paddasslem6  39330  paddasslem7  39331  paddasslem8  39332  paddasslem9  39333  paddasslem15  39339  pmodlem2  39352  pmodl42N  39356  pmapjoin  39357  llnmod1i2  39365  2polcon4bN  39423  polcon2bN  39425  poml4N  39458  poml6N  39460  osumcllem1N  39461  osumcllem2N  39462  osumcllem11N  39471  osumclN  39472  pmapojoinN  39473  pexmidlem2N  39476  pexmidlem3N  39477  pexmidlem4N  39478  pexmidlem6N  39480  pexmidlem7N  39481  pl42lem2N  39485  pl42lem3N  39486  pl42lem4N  39487  pl42N  39488  lhpexle2lem  39514  lhpexle3lem  39516  lhpexle3  39517  lhpmcvr3  39530  lhp2at0nle  39540  lhprelat3N  39545  4atex  39581  4atex2  39582  lauteq  39600  lautco  39602  ltrncoidN  39633  ltrneq2  39653  ltrnnidn  39679  ltrnideq  39680  trlnid  39684  ltrnatlw  39688  trlnle  39691  trlval3  39692  trlval4  39693  cdlemc  39702  cdlemd5  39707  cdlemd9  39711  ltrneq3  39713  cdleme0moN  39730  cdleme20  39829  cdleme21j  39841  cdleme21  39842  cdleme27cl  39871  cdlemefrs29bpre0  39901  cdlemefs27cl  39918  cdlemefs32sn1aw  39919  cdleme43fsv1snlem  39925  cdleme32d  39949  cdleme32f  39951  cdleme32le  39952  cdleme35h2  39962  cdleme38n  39969  cdleme40m  39972  cdleme41snaw  39981  cdleme42ke  39990  cdleme17d3  40001  cdleme48fvg  40005  cdlemeg46fvcl  40011  cdlemeg46fgN  40039  cdleme48gfv1  40041  cdleme48fgv  40043  cdleme50trn3  40058  trlord  40074  ltrniotavalbN  40089  cdlemb3  40111  cdlemg6c  40125  cdlemg6  40128  cdlemg7N  40131  cdlemg8c  40134  cdlemg8  40136  cdlemg11a  40142  cdlemg11b  40147  cdlemg12e  40152  cdlemg15a  40160  cdlemg15  40161  cdlemg16  40162  cdlemg16z  40164  cdlemg16zz  40165  cdlemg17dN  40168  cdlemg18a  40183  cdlemg20  40190  cdlemg22  40192  cdlemg24  40193  cdlemg37  40194  cdlemg31d  40205  cdlemg29  40210  cdlemg33b  40212  cdlemg33  40216  cdlemg38  40220  cdlemg39  40221  cdlemg40  40222  trlco  40232  trlcone  40233  cdlemg42  40234  cdlemg44b  40237  ltrncom  40243  trljco  40245  tendococl  40277  tendoplcl  40286  tendoplcom  40287  cdlemj2  40327  cdlemj3  40328  tendoid0  40330  tendoconid  40334  tendotr  40335  cdlemk25-3  40409  cdlemk26b-3  40410  cdlemk34  40415  cdlemk36  40418  cdlemk38  40420  cdlemkid4  40439  cdlemk35s-id  40443  cdlemk39s-id  40445  cdlemk19x  40448  cdlemk53  40462  cdlemk55  40466  cdlemk55u  40471  cdlemk39u  40473  cdlemk19u  40475  cdlemk56  40476  tendoex  40480  cdleml3N  40483  cdleml5N  40485  tendospcanN  40528  cdlemm10N  40623  cdlemn11pre  40715  dihord2pre  40730  dihvalcqpre  40740  dihopelvalcpre  40753  dihord6apre  40761  dihord5b  40764  dihord5apre  40767  dihord  40769  dihmeetlem1N  40795  dihglblem5apreN  40796  dihglblem3N  40800  dihmeetlem2N  40804  dihglbcpreN  40805  dihmeetbN  40808  dihmeetlem4preN  40811  dihmeetlem5  40813  dihmeetlem7N  40815  dihmeetlem10N  40821  dihmeetlem11N  40822  dihmeetlem12N  40823  dihmeetlem13N  40824  dihmeetlem15N  40826  dihmeetlem16N  40827  dihmeetlem17N  40828  dihmeetlem18N  40829  dihmeetlem19N  40830  dihmeetALTN  40832  dih1dimatlem0  40833  dihlspsnssN  40837  dihlspsnat  40838  mapdh8ad  41284  hdmap14lem14  41386  hgmapvvlem3  41430  aks6d1c6isolem1  41678  dvdsexpnn  41931  resubcan2  41974  mzprename  42200  eldioph2lem1  42211  lzunuz  42219  rencldnfi  42272  pellexlem2  42281  infmrgelbi  42329  pellfundglb  42336  pellfund14gap  42338  qirropth  42359  rmxycomplete  42369  congadd  42418  acongeq  42435  jm2.19  42445  jm2.23  42448  jm2.20nn  42449  jm2.27  42460  jm3.1  42472  aomclem6  42514  lnmepi  42540  lmhmfgsplit  42541  lmhmlnmsplit  42542  pwssplit4  42544  hbtlem2  42579  hbtlem5  42583  dgraa0p  42604  proot1hash  42654  iocunico  42670  oasubex  42746  oege1  42766  relexpxpmin  43178  brtrclfv2  43188  ntrclsiso  43528  ntrclskb  43530  ntrclsk3  43531  k0004lem3  43610  grur1cld  43700  ismnu  43729  grumnudlem  43753  suprnmpt  44577  wessf1ornlem  44588  projf1o  44600  snunioo1  44926  iccintsng  44937  lptre2pt  45057  limcleqr  45061  fnlimfvre  45091  limsupgtlem  45194  volioc  45389  iblspltprt  45390  stoweidlem19  45436  stoweidlem20  45437  stoweidlem22  45439  stoweidlem28  45445  stoweidlem34  45451  stoweidlem44  45461  stoweidlem60  45477  wallispilem3  45484  fourierdlem41  45565  fourierdlem42  45566  fourierdlem49  45572  fourierdlem51  45574  fourierdlem54  45577  fourierdlem74  45597  fourierdlem97  45620  caratheodorylem2  45944  ovnsubaddlem2  45988  hspmbllem2  46044  smflimmpt  46227  smflimsupmpt  46246  smfliminfmpt  46249  funfocofob  46487  fzopredsuc  46732  fzoopth  46736  imasetpreimafvbijlemfv  46771  iccpartigtl  46792  lighneal  46980  oexpnegALTV  47046  oexpnegnz  47047  tgblthelfgott  47184  lidldomn1  47371  ofaddmndmap  47485  lincdifsn  47570  lincellss  47572  lincresunit3lem3  47620  islindeps2  47629  lindssnlvec  47632  fdivmptf  47692  refdivmptf  47693  rrx2linest  47893  itsclc0yqsollem1  47913  itsclc0b  47923  itsclquadb  47927  itscnhlinecirc02plem3  47935