Theorem simpl1 1190

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl11  1247  simpl21  1250  simpl31  1253  simp1l1  1265  simp2l1  1271  simp3l1  1277  3anandirs  1471  rspc3ev  3575  2nreu  4376  predtrss  6229  frpomin  6247  f1prex  7165  cocan1  7172  weniso  7234  frrlem4  8114  frrlem10  8120  fprlem1  8125  smogt  8207  smorndom  8208  omeulem1  8422  nnmord  8472  nnmword  8473  difsnen  8849  enfixsn  8877  mapunen  8942  ac6sfi  9067  fipreima  9134  elfiun  9198  ordiso2  9283  wemaplem2  9315  en2eqpr  9772  indcardi  9806  fodomfi2  9825  iunfictbso  9879  infmap2  9983  cofsmo  10034  cfsmolem  10035  coftr  10038  fin23lem11  10082  fincssdom  10088  fin23lem26  10090  isf32lem9  10126  ac6num  10244  gchdomtri  10394  gchpwdom  10435  winainflem  10458  tskuni  10548  gruima  10567  gruf  10576  grudomon  10582  elnpi  10753  distrlem4pr  10791  prlem934  10798  addcan  11168  addcan2  11169  divmulass  11665  divmulasscom  11666  ltmul1a  11833  suprleub  11950  supmul1  11953  suprzcl  12409  uzsupss  12689  xleadd1a  12996  xlesubadd  13006  xmulasslem3  13029  xlemul2a  13032  xadddilem  13037  xadddi2  13040  ixxun  13104  icoshftf1o  13215  ioounsn  13218  snunioc  13221  lincmb01cmp  13236  iccf1o  13237  nn0p1elfzo  13439  fzofzim  13443  ltexp2a  13893  leexp2  13898  ltexp2r  13900  exple1  13903  expnlbnd2  13958  fun2dmnop0  14217  ccatass  14302  ccat2s1fvwOLD  14359  swrdswrdlem  14426  ccatopth  14438  repswpfx  14507  2cshw  14535  cshimadifsn  14551  cshimadifsn0  14552  cshco  14558  repsco  14562  s2f1o  14638  limsupgre  15199  addcn2  15312  mulcn2  15314  ntrivcvgmul  15623  binomrisefac  15761  dvdsmodexp  15980  dvdsadd2b  16024  dvdsexp2im  16045  dvdsmod  16047  oexpneg  16063  sadass  16187  gcdass  16264  rplpwr  16276  lcmfunsnlem1  16351  coprmdvds2  16368  rpmulgcd2  16370  qredeq  16371  rpdvds  16374  cncongr2  16382  rpexp  16436  prmdiveq  16496  hashgcdlem  16498  odzdvds  16505  modprmn0modprm0  16517  coprimeprodsq2  16519  pythagtriplem3  16528  pcdvdsb  16579  pcgcd1  16587  qexpz  16611  pockthg  16616  vdwnnlem1  16705  0ram  16730  ramz2  16734  lubss  18240  lubun  18242  clatleglb  18245  clatglbss  18246  mrelatglb  18287  isnsgrp  18388  issubmnd  18421  ress0g  18422  gsumccatOLD  18488  gsumccat  18489  frmdss2  18511  submefmnd  18543  mulgneg  18731  mulgdirlem  18743  submmulg  18756  subgmulg  18778  nmzsubg  18802  ghmmulg  18855  gsmsymgreqlem1  19047  pmtrfb  19082  psgnunilem4  19114  odmodnn0  19157  odnncl  19162  odmod  19163  odmulgid  19170  odmulgeq  19173  odf1o1  19186  odf1o2  19187  odngen  19191  gexdvdsi  19197  pgpfi1  19209  odcau  19218  subgslw  19230  fislw  19239  lsmssv  19257  lsmless1x  19258  lsmless2x  19259  lsmsubm  19267  lsmmod  19290  lsmmod2  19291  efgred  19363  cntzcmn  19450  ghmplusg  19456  odadd1  19458  odadd2  19459  odadd  19460  lsmcomx  19466  gsumconst  19544  ablsimpgprmd  19727  srg1zr  19774  ring1eq0  19838  mulgass2  19849  isabvd  20089  rmodislmodlem  20199  rmodislmod  20200  rmodislmodOLD  20201  lssintcl  20235  0lmhm  20311  lmhmvsca  20316  reslmhm2b  20325  pwssplit1  20330  pwssplit3  20332  lspfixed  20399  lspsnat  20416  lidldvgen  20535  xrsdsreclblem  20653  regsumsupp  20836  obselocv  20944  uvcresum  21009  frlmsslsp  21012  frlmup4  21017  lindff1  21036  f1lindf  21038  lsslindf  21046  islindf4  21054  lbslcic  21057  issubassa  21082  evlsval2  21306  psrplusgpropd  21416  coe1subfv  21446  coe1mul2  21449  mhmvlin  21555  mpomatmul  21604  mamutpos  21616  scmatscmide  21665  mavmulsolcl  21709  marrepcl  21722  mdetdiag  21757  mdetunilem1  21770  mdetunilem3  21772  mdetunilem7  21776  mdetunilem9  21778  mdetmul  21781  slesolinvbi  21839  m2pmfzmap  21905  pmatcollpwlem  21938  pmatcollpw  21939  mp2pm2mplem4  21967  chpdmatlem3  21998  chfacfisfcpmat  22013  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmidpmatlem2  22029  cpmadugsumlemB  22032  cpmadugsumlemC  22033  cpmadugsumlemF  22034  riinopn  22066  neiint  22264  topssnei  22284  restntr  22342  iscnp4  22423  cnconst2  22443  cnrest2  22446  cnprest2  22450  cnpdis  22453  cnt0  22506  cnt1  22510  cnhaus  22514  ordthauslem  22543  cncmp  22552  fiuncmp  22564  sscmp  22565  hauscmp  22567  cnconn  22582  unconn  22589  nlly2i  22636  llynlly  22637  nllyidm  22649  finlocfin  22680  ptrescn  22799  xkococnlem  22819  qtopss  22875  kqfvima  22890  r0cld  22898  ordthmeolem  22961  fbssint  22998  fmf  23105  fmss  23106  elfm  23107  rnelfmlem  23112  rnelfm  23113  fmco  23121  flimss2  23132  flimss1  23133  flimrest  23143  flftg  23156  cnpflf2  23160  cnpflf  23161  flfcnp  23164  supnfcls  23180  fclsss1  23182  fclsss2  23183  fcfnei  23195  fcfelbas  23196  cnpfcfi  23200  subgntr  23267  opnsubg  23268  cldsubg  23271  ghmcnp  23275  utop2nei  23411  neipcfilu  23457  bldisj  23560  blgt0  23561  bl2in  23562  blss2ps  23565  blss2  23566  blssps  23586  blss  23587  xmetresbl  23599  lpbl  23668  blcld  23670  stdbdbl  23682  metcnp3  23705  metcnp2  23707  txmetcnp  23712  blval2  23727  nmoix  23902  nmoeq0  23909  icoopnst  24111  iocopnst  24112  xrhmeo  24118  nmhmcn  24292  cphsqrtcl2  24359  cphsqrtcl3  24360  cfil3i  24442  caublcls  24482  bcthlem5  24501  cmetcusp1  24526  cssbn  24548  rrxcph  24565  pjth  24612  ovoliunlem2  24676  volun  24718  volsup2  24778  mbfimaopn2  24830  iblconst  24991  itgconst  24992  dvcnp2  25093  dvcn  25094  deg1mul3le  25290  deg1tmle  25291  dvdsq1p  25334  ig1peu  25345  ig1pdvds  25350  coeid3  25410  dgrmulc  25441  efcvx  25617  tanord  25703  logdivlti  25784  logccv  25827  recxpcl  25839  cxpeq  25919  ang180  25973  isosctrlem2  25978  cxp2lim  26135  amgm  26149  muval1  26291  dvdssqf  26296  mumullem2  26338  mumul  26339  bcmono  26434  lgsfcl2  26460  lgsdilem  26481  lgsdirprm  26488  lgsdir  26489  lgsdi  26491  lgsne0  26492  padicabv  26787  brbtwn2  27282  colinearalglem1  27283  colinearalg  27287  axcgrtr  27292  axsegconlem8  27301  axsegconlem9  27302  axsegconlem10  27303  axcontlem8  27348  axcontlem10  27350  elntg2  27362  vtxdlfuhgr1v  27855  umgr2wlk  28323  erclwwlksym  28394  clwwlkfo  28423  clwwlkext2edg  28429  erclwwlknsym  28443  clwwlknon1  28470  numclwwlk2lem1  28749  numclwwlk5  28761  frgrregord13  28769  nvmul0or  29021  ipval2lem2  29075  lnomul  29131  shless  29730  shlej1  29731  pjspansn  29948  hoadddi  30174  kbmul  30326  homco2  30348  kbass2  30488  eliccelico  31107  elicoelioo  31108  iocinioc2  31109  iocinif  31111  swrdrn2  31235  xrge0adddir  31310  xrge0npcan  31312  archiabl  31461  ress1r  31495  rhmdvdsr  31526  pidlnz  31580  grplsm0l  31600  intlidl  31611  ssmxidl  31651  pstmfval  31855  fmcncfil  31890  zrhnm  31928  qqhnm  31949  measvunilem  32189  volfiniune  32207  dya2iocnrect  32257  sibfinima  32315  probun  32395  probinc  32397  cndprob01  32411  signstfvp  32559  bnj517  32874  bnj594  32901  pconnpi1  33208  cvmsss2  33245  mrsubcv  33481  msubvrs  33531  br6  33733  br4  33734  nosep1o  33893  nosep2o  33894  nosepssdm  33898  nolt02olem  33906  nosupres  33919  nosupbnd1lem1  33920  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd1lem6  33925  nosupbnd2  33928  noinfres  33934  noinfbnd1lem1  33935  noinfbnd1lem4  33938  noinfbnd1lem6  33940  noinfbnd2  33943  noetasuplem3  33947  noetalem1  33953  scutbdaybnd  34018  sltlpss  34096  coinitsslt  34098  cgrcomim  34300  cgrtriv  34313  cgrextend  34319  segconeq  34321  btwntriv2  34323  btwnintr  34330  btwnexch3  34331  btwnouttr2  34333  trisegint  34339  cgrsub  34356  cgrxfr  34366  btwnxfr  34367  lineext  34387  btwnconn1lem13  34410  btwnconn1lem14  34411  btwnconn3  34414  segcon2  34416  brsegle  34419  brsegle2  34420  segletr  34425  segleantisym  34426  seglelin  34427  outsideofeu  34442  lineunray  34458  lineelsb2  34459  ivthALT  34533  lindsenlbs  35781  areacirc  35879  cocanfo  35885  upixp  35896  ismtyima  35970  rrndstprj2  35998  zerdivemp1x  36114  lsatfixedN  37030  lssat  37037  eqlkr  37120  eqlkr2  37121  lkrlsp  37123  lshpkrlem4  37134  opposet  37202  cvrcon3b  37298  cvrcmp  37304  atlen0  37331  atnle  37338  atlatmstc  37340  cvlatexch3  37359  cvlsupr2  37364  hlsupr2  37408  hlrelat2  37424  cvrexchlem  37440  lnnat  37448  atcvrj2b  37453  atle  37457  atexchcvrN  37461  atbtwn  37467  athgt  37477  3dimlem3  37482  3dim1  37488  1cvratlt  37495  1cvrjat  37496  ps-1  37498  ps-2  37499  3atlem3  37506  3atlem5  37508  3atlem7  37510  llni  37529  llni2  37533  atcvrlln2  37540  llnexatN  37542  llncmp  37543  2llnmat  37545  2at0mat0  37546  lplni  37553  lplnnle2at  37562  2atnelpln  37565  lplnllnneN  37577  llncvrlpln2  37578  2lplnmN  37580  2llnmj  37581  lplncmp  37583  lplnexatN  37584  lplnexllnN  37585  2llnm3N  37590  lvoli  37596  lvoli3  37598  islvol2aN  37613  4atlem0a  37614  4atlem3  37617  4atlem3a  37618  4atlem4a  37620  4atlem4b  37621  4atlem4c  37622  4atlem4d  37623  4atlem10b  37626  4atlem11  37630  4atlem12  37633  lplncvrlvol2  37636  lvolcmp  37638  2lplnmj  37643  islinei  37761  pmapglbx  37790  linepmap  37796  lneq2at  37799  lnjatN  37801  lncvrat  37803  lncmp  37804  2llnma3r  37809  elpaddatriN  37824  elpaddat  37825  paddcom  37834  paddss1  37838  paddss2  37839  paddss12  37840  paddasslem6  37846  paddasslem7  37847  paddasslem8  37848  paddasslem9  37849  paddasslem15  37855  pmodlem2  37868  pmodl42N  37872  pmapjoin  37873  llnmod1i2  37881  2polcon4bN  37939  polcon2bN  37941  poml4N  37974  poml6N  37976  osumcllem1N  37977  osumcllem2N  37978  osumcllem11N  37987  osumclN  37988  pmapojoinN  37989  pexmidlem2N  37992  pexmidlem3N  37993  pexmidlem4N  37994  pexmidlem6N  37996  pexmidlem7N  37997  pl42lem2N  38001  pl42lem3N  38002  pl42lem4N  38003  pl42N  38004  lhpexle2lem  38030  lhpexle3lem  38032  lhpexle3  38033  lhpmcvr3  38046  lhp2at0nle  38056  lhprelat3N  38061  4atex  38097  4atex2  38098  lauteq  38116  lautco  38118  ltrncoidN  38149  ltrneq2  38169  ltrnnidn  38195  ltrnideq  38196  trlnid  38200  ltrnatlw  38204  trlnle  38207  trlval3  38208  trlval4  38209  cdlemc  38218  cdlemd5  38223  cdlemd9  38227  ltrneq3  38229  cdleme0moN  38246  cdleme20  38345  cdleme21j  38357  cdleme21  38358  cdleme27cl  38387  cdlemefrs29bpre0  38417  cdlemefs27cl  38434  cdlemefs32sn1aw  38435  cdleme43fsv1snlem  38441  cdleme32d  38465  cdleme32f  38467  cdleme32le  38468  cdleme35h2  38478  cdleme38n  38485  cdleme40m  38488  cdleme41snaw  38497  cdleme42ke  38506  cdleme17d3  38517  cdleme48fvg  38521  cdlemeg46fvcl  38527  cdlemeg46fgN  38555  cdleme48gfv1  38557  cdleme48fgv  38559  cdleme50trn3  38574  trlord  38590  ltrniotavalbN  38605  cdlemb3  38627  cdlemg6c  38641  cdlemg6  38644  cdlemg7N  38647  cdlemg8c  38650  cdlemg8  38652  cdlemg11a  38658  cdlemg11b  38663  cdlemg12e  38668  cdlemg15a  38676  cdlemg15  38677  cdlemg16  38678  cdlemg16z  38680  cdlemg16zz  38681  cdlemg17dN  38684  cdlemg18a  38699  cdlemg20  38706  cdlemg22  38708  cdlemg24  38709  cdlemg37  38710  cdlemg31d  38721  cdlemg29  38726  cdlemg33b  38728  cdlemg33  38732  cdlemg38  38736  cdlemg39  38737  cdlemg40  38738  trlco  38748  trlcone  38749  cdlemg42  38750  cdlemg44b  38753  ltrncom  38759  trljco  38761  tendococl  38793  tendoplcl  38802  tendoplcom  38803  cdlemj2  38843  cdlemj3  38844  tendoid0  38846  tendoconid  38850  tendotr  38851  cdlemk25-3  38925  cdlemk26b-3  38926  cdlemk34  38931  cdlemk36  38934  cdlemk38  38936  cdlemkid4  38955  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk19x  38964  cdlemk53  38978  cdlemk55  38982  cdlemk55u  38987  cdlemk39u  38989  cdlemk19u  38991  cdlemk56  38992  tendoex  38996  cdleml3N  38999  cdleml5N  39001  tendospcanN  39044  cdlemm10N  39139  cdlemn11pre  39231  dihord2pre  39246  dihvalcqpre  39256  dihopelvalcpre  39269  dihord6apre  39277  dihord5b  39280  dihord5apre  39283  dihord  39285  dihmeetlem1N  39311  dihglblem5apreN  39312  dihglblem3N  39316  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetbN  39324  dihmeetlem4preN  39327  dihmeetlem5  39329  dihmeetlem7N  39331  dihmeetlem10N  39337  dihmeetlem11N  39338  dihmeetlem12N  39339  dihmeetlem13N  39340  dihmeetlem15N  39342  dihmeetlem16N  39343  dihmeetlem17N  39344  dihmeetlem18N  39345  dihmeetlem19N  39346  dihmeetALTN  39348  dih1dimatlem0  39349  dihlspsnssN  39353  dihlspsnat  39354  mapdh8ad  39800  hdmap14lem14  39902  hgmapvvlem3  39946  dvdsexpnn  40347  resubcan2  40378  mzprename  40578  eldioph2lem1  40589  lzunuz  40597  rencldnfi  40650  pellexlem2  40659  infmrgelbi  40707  pellfundglb  40714  pellfund14gap  40716  qirropth  40737  rmxycomplete  40746  congadd  40795  acongeq  40812  jm2.19  40822  jm2.23  40825  jm2.20nn  40826  jm2.27  40837  jm3.1  40849  aomclem6  40891  lnmepi  40917  lmhmfgsplit  40918  lmhmlnmsplit  40919  pwssplit4  40921  hbtlem2  40956  hbtlem5  40960  dgraa0p  40981  proot1hash  41032  iocunico  41049  relexpxpmin  41332  brtrclfv2  41342  ntrclsiso  41684  ntrclskb  41686  ntrclsk3  41687  k0004lem3  41766  grur1cld  41857  ismnu  41886  grumnudlem  41910  suprnmpt  42717  wessf1ornlem  42729  projf1o  42743  snunioo1  43057  iccintsng  43068  lptre2pt  43188  limcleqr  43192  fnlimfvre  43222  limsupgtlem  43325  volioc  43520  iblspltprt  43521  stoweidlem19  43567  stoweidlem20  43568  stoweidlem22  43570  stoweidlem28  43576  stoweidlem34  43582  stoweidlem44  43592  stoweidlem60  43608  wallispilem3  43615  fourierdlem41  43696  fourierdlem42  43697  fourierdlem49  43703  fourierdlem51  43705  fourierdlem54  43708  fourierdlem74  43728  fourierdlem97  43751  caratheodorylem2  44072  ovnsubaddlem2  44116  hspmbllem2  44172  smflimmpt  44354  smflimsupmpt  44373  smfliminfmpt  44376  funfocofob  44581  fzopredsuc  44826  fzoopth  44830  imasetpreimafvbijlemfv  44865  iccpartigtl  44886  lighneal  45074  oexpnegALTV  45140  oexpnegnz  45141  tgblthelfgott  45278  lidldomn1  45490  ofaddmndmap  45690  lincdifsn  45776  lincellss  45778  lincresunit3lem3  45826  islindeps2  45835  lindssnlvec  45838  fdivmptf  45898  refdivmptf  45899  rrx2linest  46099  itsclc0yqsollem1  46119  itsclc0b  46129  itsclquadb  46133  itscnhlinecirc02plem3  46141