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  3596  2nreu  4405  predtrss  6324  frpomin  6342  f1prex  7289  cocan1  7296  weniso  7361  frrlem4  8292  frrlem10  8298  fprlem1  8303  smogt  8360  smocdmdom  8361  omeulem1  8573  nnmord  8624  nnmword  8625  naddasslem1  8687  naddasslem2  8688  difsnen  9061  enfixsn  9088  mapunen  9148  ac6sfi  9258  fipreima  9329  elfiun  9404  ordiso2  9491  wemaplem2  9523  en2eqpr  10014  indcardi  10048  fodomfi2  10067  iunfictbso  10121  infmap2  10223  cofsmo  10275  cfsmolem  10276  coftr  10279  fin23lem11  10323  fincssdom  10329  fin23lem26  10331  isf32lem9  10367  ac6num  10485  gchdomtri  10642  gchpwdom  10683  winainflem  10706  tskuni  10796  gruima  10815  gruf  10824  grudomon  10830  elnpi  11001  distrlem4pr  11039  prlem934  11046  addcan  11422  addcan2  11423  divmulass  11923  divmulasscom  11924  ltmul1a  12092  suprleub  12209  supmul1  12212  suprzcl  12705  uzsupss  12993  xleadd1a  13309  xlesubadd  13319  xmulasslem3  13342  xlemul2a  13345  xadddilem  13350  xadddi2  13353  ixxun  13418  icoshftf1o  13531  ioounsn  13534  snunioc  13537  lincmb01cmp  13552  iccf1o  13553  nn0p1elfzo  13762  fzofzim  13769  fzoopth  13822  ltexp2a  14234  leexp2  14239  ltexp2r  14241  exple1  14245  expnlbnd2  14302  fun2dmnop0  14573  ccatass  14658  swrdswrdlem  14777  ccatopth  14789  repswpfx  14860  2cshw  14888  cshimadifsn  14904  cshimadifsn0  14905  cshco  14911  repsco  14915  s2f1o  14991  limsupgre  15572  addcn2  15685  mulcn2  15687  ntrivcvgmul  15995  binomrisefac  16134  dvdsmodexp  16356  dvdsadd2b  16402  dvdsexp2im  16423  dvdsmod  16425  oexpneg  16441  sadass  16567  gcdass  16643  rplpwr  16654  lcmfunsnlem1  16733  coprmdvds2  16750  rpmulgcd2  16752  qredeq  16753  rpdvds  16756  cncongr2  16764  rpexp  16819  prmdiveq  16883  hashgcdlem  16885  odzdvds  16893  modprmn0modprm0  16905  coprimeprodsq2  16907  pythagtriplem3  16916  pcdvdsb  16967  pcgcd1  16975  qexpz  16999  pockthg  17004  vdwnnlem1  17093  0ram  17118  ramz2  17122  lubss  18607  lubun  18609  clatleglb  18612  clatglbss  18613  mrelatglb  18654  isnsgrp  18831  issubmnd  18872  ress0gOLD  18874  mhmvlin  18915  gsumccat  18956  frmdss2  18978  submefmnd  19010  mulgneg  19221  mulgdirlem  19234  submmulg  19247  subgmulg  19270  nmzsubg  19294  ghmmulg  19361  gsmsymgreqlem1  19563  pmtrfb  19598  psgnunilem4  19630  odmodnn0  19673  odnncl  19678  odmod  19679  odmulgid  19687  odmulgeq  19690  odf1o1  19705  odf1o2  19706  odngen  19710  gexdvdsi  19716  pgpfi1  19728  odcau  19737  subgslw  19749  fislw  19758  lsmssv  19776  lsmless1x  19777  lsmless2x  19778  lsmsubm  19786  lsmmod  19808  lsmmod2  19809  efgred  19881  cntzcmn  19973  ghmplusg  19979  odadd1  19981  odadd2  19982  odadd  19983  lsmcomx  19989  gsumconst  20067  ablsimpgprmd  20250  ring1eq0  20446  mulgass2  20457  rngisom1  20613  rhmdvdsr  20674  isabvd  20984  rmodislmodlem  21119  rmodislmod  21120  lssintcl  21154  0lmhm  21230  lmhmvsca  21235  reslmhm2b  21244  pwssplit1  21249  pwssplit3  21251  lspfixed  21321  lspsnat  21338  unichnlidl  21431  pidlnz  21443  rnglidlrng  21450  2idlcpblrng  21479  lidldvgen  21571  xrsdsreclblem  21632  regsumsupp  21841  obselocv  21947  uvcresum  22012  frlmsslsp  22015  frlmup4  22020  lindff1  22039  f1lindf  22041  lsslindf  22049  islindf4  22057  lbslcic  22060  lindsenlbs  22070  issubassa  22088  evlsval2  22309  psrplusgpropd  22466  coe1subfv  22498  coe1mul2  22501  mpomatmul  22674  mamutpos  22686  scmatscmide  22735  mavmulsolcl  22779  marrepcl  22792  mdetdiag  22827  mdetunilem1  22840  mdetunilem3  22842  mdetunilem7  22846  mdetunilem9  22848  mdetmul  22851  slesolinvbi  22912  m2pmfzmap  22978  pmatcollpwlem  23011  pmatcollpw  23012  mp2pm2mplem4  23040  chpdmatlem3  23071  chfacfisfcpmat  23086  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  chfacfpmmulgsum2  23096  cayhamlem1  23097  cpmidpmatlem2  23102  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  riinopn  23139  neiint  23335  topssnei  23355  restntr  23413  iscnp4  23494  cnconst2  23514  cnrest2  23517  cnprest2  23521  cnpdis  23524  cnt0  23577  cnt1  23581  cnhaus  23585  ordthauslem  23614  cncmp  23623  fiuncmp  23635  sscmp  23636  hauscmp  23638  cnconn  23653  unconn  23660  nlly2i  23708  llynlly  23709  nllyidm  23721  finlocfin  23752  ptrescn  23871  xkococnlem  23891  qtopss  23947  kqfvima  23962  r0cld  23970  ordthmeolem  24033  fbssint  24070  fmf  24177  fmss  24178  elfm  24179  rnelfmlem  24184  rnelfm  24185  fmco  24193  flimss2  24204  flimss1  24205  flimrest  24215  flftg  24228  cnpflf2  24232  cnpflf  24233  flfcnp  24236  supnfcls  24252  fclsss1  24254  fclsss2  24255  fcfnei  24267  fcfelbas  24268  cnpfcfi  24272  subgntr  24339  opnsubg  24340  cldsubg  24343  ghmcnp  24347  utop2nei  24482  neipcfilu  24527  bldisj  24630  blgt0  24631  bl2in  24632  blss2ps  24635  blss2  24636  blssps  24656  blss  24657  xmetresbl  24669  lpbl  24735  blcld  24737  stdbdbl  24749  metcnp3  24772  metcnp2  24774  txmetcnp  24779  blval2  24794  nmoix  24961  nmoeq0  24968  icoopnst  25173  iocopnst  25174  xrhmeo  25180  nmhmcn  25354  cphsqrtcl2  25420  cphsqrtcl3  25421  cfil3i  25503  caublcls  25543  bcthlem5  25562  cmetcusp1  25587  cssbn  25609  rrxcph  25626  pjth  25673  ovoliunlem2  25737  volun  25779  volsup2  25839  mbfimaopn2  25891  iblconst  26052  itgconst  26053  dvcnp2  26154  dvcn  26155  deg1mul3le  26349  deg1tmle  26350  dvdsq1p  26395  ig1peu  26407  ig1pdvds  26412  coeid3  26473  dgrmulc  26504  efcvx  26692  tanord  26783  logdivlti  26865  logccv  26908  recxpcl  26920  cxpeq  27002  ang180  27059  isosctrlem2  27064  cxp2lim  27221  amgm  27235  muval1  27377  dvdssqf  27382  mumullem2  27424  mumul  27425  bcmono  27521  lgsfcl2  27547  lgsdilem  27568  lgsdirprm  27575  lgsdir  27576  lgsdi  27578  lgsne0  27579  padicabv  27874  nosep1o  27925  nosep2o  27926  nosepssdm  27930  nolt02olem  27938  nosupres  27951  nosupbnd1lem1  27952  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd1lem6  27957  nosupbnd2  27960  noinfres  27966  noinfbnd1lem1  27967  noinfbnd1lem4  27970  noinfbnd1lem6  27972  noinfbnd2  27975  noetasuplem3  27979  noetalem1  27985  cutbdaybnd  28068  ltslpss  28181  leslss  28182  coinitslts  28192  addsass  28278  addsdi  28428  mulsass  28439  norecdiv  28463  bdayfinbndlem1  28740  z12bdaylem  28757  brbtwn2  29370  colinearalglem1  29371  colinearalg  29375  axcgrtr  29380  axsegconlem8  29389  axsegconlem9  29390  axsegconlem10  29391  axcontlem8  29436  axcontlem10  29438  elntg2  29450  vtxdlfuhgr1v  29947  umgr2wlk  30425  erclwwlksym  30499  clwwlkfo  30528  clwwlkext2edg  30534  erclwwlknsym  30548  clwwlknon1  30575  numclwwlk2lem1  30864  numclwwlk5  30876  frgrregord13  30884  nvmul0or  31139  ipval2lem2  31193  lnomul  31249  shless  31848  shlej1  31849  pjspansn  32066  hoadddi  32292  kbmul  32444  homco2  32466  kbass2  32606  eliccelico  33256  elicoelioo  33257  iocinioc2  33258  iocinif  33260  swrdrn2  33404  xrge0adddir  33466  xrge0npcan  33468  archiabl  33646  ress1r  33680  grplsm0l  33840  intlidl  33856  ssmxidl  33885  pstmfval  34414  fmcncfil  34449  zrhnm  34485  qqhnm  34508  measvunilem  34731  volfiniune  34749  dya2iocnrect  34800  sibfinima  34858  probun  34938  probinc  34940  cndprob01  34954  signstfvp  35087  bnj517  35402  bnj594  35429  fissorduni  35602  pconnpi1  35824  cvmsss2  35861  mrsubcv  36097  msubvrs  36147  br6  36344  br4  36345  cgrcomim  36577  cgrtriv  36590  cgrextend  36596  segconeq  36598  btwntriv2  36600  btwnintr  36607  btwnexch3  36608  btwnouttr2  36610  trisegint  36616  cgrsub  36633  cgrxfr  36643  btwnxfr  36644  lineext  36664  btwnconn1lem13  36687  btwnconn1lem14  36688  btwnconn3  36691  segcon2  36693  brsegle  36696  brsegle2  36697  segletr  36702  segleantisym  36703  seglelin  36704  outsideofeu  36719  lineunray  36735  lineelsb2  36736  nmulss1  36802  ltnmul  36804  nmulle  36805  ltnadd  36806  naddle  36807  nadddi  36812  ivthALT  36962  weiunpo  37092  weiunso  37093  weiunfr  37094  weiunse  37095  areacirc  38470  cocanfo  38477  upixp  38487  ismtyima  38561  rrndstprj2  38589  zerdivemp1x  38705  lsatfixedN  39890  lssat  39897  eqlkr  39980  eqlkr2  39981  lkrlsp  39983  lshpkrlem4  39994  opposet  40062  cvrcon3b  40158  cvrcmp  40164  atlen0  40191  atnle  40198  atlatmstc  40200  cvlatexch3  40219  cvlsupr2  40224  hlsupr2  40268  hlrelat2  40284  cvrexchlem  40300  lnnat  40308  atcvrj2b  40313  atle  40317  atexchcvrN  40321  atbtwn  40327  athgt  40337  3dimlem3  40342  3dim1  40348  1cvratlt  40355  1cvrjat  40356  ps-1  40358  ps-2  40359  3atlem3  40366  3atlem5  40368  3atlem7  40370  llni  40389  llni2  40393  atcvrlln2  40400  llnexatN  40402  llncmp  40403  2llnmat  40405  2at0mat0  40406  lplni  40413  lplnnle2at  40422  2atnelpln  40425  lplnllnneN  40437  llncvrlpln2  40438  2lplnmN  40440  2llnmj  40441  lplncmp  40443  lplnexatN  40444  lplnexllnN  40445  2llnm3N  40450  lvoli  40456  lvoli3  40458  islvol2aN  40473  4atlem0a  40474  4atlem3  40477  4atlem3a  40478  4atlem4a  40480  4atlem4b  40481  4atlem4c  40482  4atlem4d  40483  4atlem10b  40486  4atlem11  40490  4atlem12  40493  lplncvrlvol2  40496  lvolcmp  40498  2lplnmj  40503  islinei  40621  pmapglbx  40650  linepmap  40656  lneq2at  40659  lnjatN  40661  lncvrat  40663  lncmp  40664  2llnma3r  40669  elpaddatriN  40684  elpaddat  40685  paddcom  40694  paddss1  40698  paddss2  40699  paddss12  40700  paddasslem6  40706  paddasslem7  40707  paddasslem8  40708  paddasslem9  40709  paddasslem15  40715  pmodlem2  40728  pmodl42N  40732  pmapjoin  40733  llnmod1i2  40741  2polcon4bN  40799  polcon2bN  40801  poml4N  40834  poml6N  40836  osumcllem1N  40837  osumcllem2N  40838  osumcllem11N  40847  osumclN  40848  pmapojoinN  40849  pexmidlem2N  40852  pexmidlem3N  40853  pexmidlem4N  40854  pexmidlem6N  40856  pexmidlem7N  40857  pl42lem2N  40861  pl42lem3N  40862  pl42lem4N  40863  pl42N  40864  lhpexle2lem  40890  lhpexle3lem  40892  lhpexle3  40893  lhpmcvr3  40906  lhp2at0nle  40916  lhprelat3N  40921  4atex  40957  4atex2  40958  lauteq  40976  lautco  40978  ltrncoidN  41009  ltrneq2  41029  ltrnnidn  41055  ltrnideq  41056  trlnid  41060  ltrnatlw  41064  trlnle  41067  trlval3  41068  trlval4  41069  cdlemc  41078  cdlemd5  41083  cdlemd9  41087  ltrneq3  41089  cdleme0moN  41106  cdleme20  41205  cdleme21j  41217  cdleme21  41218  cdleme27cl  41247  cdlemefrs29bpre0  41277  cdlemefs27cl  41294  cdlemefs32sn1aw  41295  cdleme43fsv1snlem  41301  cdleme32d  41325  cdleme32f  41327  cdleme32le  41328  cdleme35h2  41338  cdleme38n  41345  cdleme40m  41348  cdleme41snaw  41357  cdleme42ke  41366  cdleme17d3  41377  cdleme48fvg  41381  cdlemeg46fvcl  41387  cdlemeg46fgN  41415  cdleme48gfv1  41417  cdleme48fgv  41419  cdleme50trn3  41434  trlord  41450  ltrniotavalbN  41465  cdlemb3  41487  cdlemg6c  41501  cdlemg6  41504  cdlemg7N  41507  cdlemg8c  41510  cdlemg8  41512  cdlemg11a  41518  cdlemg11b  41523  cdlemg12e  41528  cdlemg15a  41536  cdlemg15  41537  cdlemg16  41538  cdlemg16z  41540  cdlemg16zz  41541  cdlemg17dN  41544  cdlemg18a  41559  cdlemg20  41566  cdlemg22  41568  cdlemg24  41569  cdlemg37  41570  cdlemg31d  41581  cdlemg29  41586  cdlemg33b  41588  cdlemg33  41592  cdlemg38  41596  cdlemg39  41597  cdlemg40  41598  trlco  41608  trlcone  41609  cdlemg42  41610  cdlemg44b  41613  ltrncom  41619  trljco  41621  tendococl  41653  tendoplcl  41662  tendoplcom  41663  cdlemj2  41703  cdlemj3  41704  tendoid0  41706  tendoconid  41710  tendotr  41711  cdlemk25-3  41785  cdlemk26b-3  41786  cdlemk34  41791  cdlemk36  41794  cdlemk38  41796  cdlemkid4  41815  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk19x  41824  cdlemk53  41838  cdlemk55  41842  cdlemk55u  41847  cdlemk39u  41849  cdlemk19u  41851  cdlemk56  41852  tendoex  41856  cdleml3N  41859  cdleml5N  41861  tendospcanN  41904  cdlemm10N  41999  cdlemn11pre  42091  dihord2pre  42106  dihvalcqpre  42116  dihopelvalcpre  42129  dihord6apre  42137  dihord5b  42140  dihord5apre  42143  dihord  42145  dihmeetlem1N  42171  dihglblem5apreN  42172  dihglblem3N  42176  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetbN  42184  dihmeetlem4preN  42187  dihmeetlem5  42189  dihmeetlem7N  42191  dihmeetlem10N  42197  dihmeetlem11N  42198  dihmeetlem12N  42199  dihmeetlem13N  42200  dihmeetlem15N  42202  dihmeetlem16N  42203  dihmeetlem17N  42204  dihmeetlem18N  42205  dihmeetlem19N  42206  dihmeetALTN  42208  dih1dimatlem0  42209  dihlspsnssN  42213  dihlspsnat  42214  mapdh8ad  42660  hdmap14lem14  42762  hgmapvvlem3  42806  aks6d1c6isolem1  43048  dvdsexpnn  43216  resubcan2  43271  mzprename  43602  eldioph2lem1  43613  lzunuz  43621  rencldnfi  43670  pellexlem2  43679  infmrgelbi  43727  pellfundglb  43734  pellfund14gap  43736  qirropth  43757  rmxycomplete  43766  congadd  43815  acongeq  43832  jm2.19  43842  jm2.23  43845  jm2.20nn  43846  jm2.27  43857  jm3.1  43869  aomclem6  43908  lnmepi  43934  lmhmfgsplit  43935  lmhmlnmsplit  43936  pwssplit4  43938  hbtlem2  43973  hbtlem5  43977  dgraa0p  43998  proot1hash  44044  iocunico  44060  oasubex  44135  oege1  44155  relexpxpmin  44565  brtrclfv2  44575  ntrclsiso  44915  ntrclskb  44917  ntrclsk3  44918  k0004lem3  44997  grur1cld  45078  ismnu  45093  grumnudlem  45117  suprnmpt  46014  wessf1ornlem  46025  projf1o  46036  snunioo1  46350  iccintsng  46361  lptre2pt  46476  limcleqr  46480  fnlimfvre  46510  limsupgtlem  46613  volioc  46808  iblspltprt  46809  stoweidlem19  46855  stoweidlem20  46856  stoweidlem22  46858  stoweidlem28  46864  stoweidlem34  46870  stoweidlem44  46880  stoweidlem60  46896  wallispilem3  46903  fourierdlem41  46984  fourierdlem42  46985  fourierdlem49  46991  fourierdlem51  46993  fourierdlem54  46996  fourierdlem74  47016  fourierdlem97  47039  caratheodorylem2  47363  ovnsubaddlem2  47407  hspmbllem2  47463  smflimmpt  47646  smflimsupmpt  47665  smfliminfmpt  47668  funfocofob  47974  fzopredsuc  48220  nnmul2b  48227  imasetpreimafvbijlemfv  48310  iccpartigtl  48331  lighneal  48522  oexpnegALTV  48601  oexpnegnz  48602  tgblthelfgott  48739  clnbgrgrim  48858  uhgrimgrlim  48911  gpgusgralem  48980  lidldomn1  49154  ofaddmndmap  49281  lincdifsn  49362  lincellss  49364  lincresunit3lem3  49412  islindeps2  49421  lindssnlvec  49424  fdivmptf  49479  refdivmptf  49480  rrx2linest  49680  itsclc0yqsollem1  49700  itsclc0b  49710  itsclquadb  49714  itscnhlinecirc02plem3  49722  diag1  50238  setc1onsubc  50536