Theorem simpl1 1193

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 1187	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  simpl11  1250  simpl21  1253  simpl31  1256  simp1l1  1268  simp2l1  1274  simp3l1  1280  3anandirs  1475  rspc3ev  3595  2nreu  4398  predtrss  6288  frpomin  6306  f1prex  7240  cocan1  7247  weniso  7310  frrlem4  8241  frrlem10  8247  fprlem1  8252  smogt  8309  smocdmdom  8310  omeulem1  8519  nnmord  8570  nnmword  8571  naddasslem1  8632  naddasslem2  8633  difsnen  8999  enfixsn  9026  mapunen  9086  ac6sfi  9196  fipreima  9270  elfiun  9345  ordiso2  9432  wemaplem2  9464  en2eqpr  9929  indcardi  9963  fodomfi2  9982  iunfictbso  10036  infmap2  10139  cofsmo  10191  cfsmolem  10192  coftr  10195  fin23lem11  10239  fincssdom  10245  fin23lem26  10247  isf32lem9  10283  ac6num  10401  gchdomtri  10552  gchpwdom  10593  winainflem  10616  tskuni  10706  gruima  10725  gruf  10734  grudomon  10740  elnpi  10911  distrlem4pr  10949  prlem934  10956  addcan  11329  addcan2  11330  divmulass  11831  divmulasscom  11832  ltmul1a  12002  suprleub  12120  supmul1  12123  suprzcl  12584  uzsupss  12865  xleadd1a  13180  xlesubadd  13190  xmulasslem3  13213  xlemul2a  13216  xadddilem  13221  xadddi2  13224  ixxun  13289  icoshftf1o  13402  ioounsn  13405  snunioc  13408  lincmb01cmp  13423  iccf1o  13424  nn0p1elfzo  13630  fzofzim  13637  fzoopth  13690  ltexp2a  14101  leexp2  14106  ltexp2r  14108  exple1  14112  expnlbnd2  14169  fun2dmnop0  14439  ccatass  14524  swrdswrdlem  14639  ccatopth  14651  repswpfx  14720  2cshw  14748  cshimadifsn  14764  cshimadifsn0  14765  cshco  14771  repsco  14775  s2f1o  14851  limsupgre  15416  addcn2  15529  mulcn2  15531  ntrivcvgmul  15837  binomrisefac  15977  dvdsmodexp  16199  dvdsadd2b  16245  dvdsexp2im  16266  dvdsmod  16268  oexpneg  16284  sadass  16410  gcdass  16486  rplpwr  16497  lcmfunsnlem1  16576  coprmdvds2  16593  rpmulgcd2  16595  qredeq  16596  rpdvds  16599  cncongr2  16607  rpexp  16661  prmdiveq  16725  hashgcdlem  16727  odzdvds  16735  modprmn0modprm0  16747  coprimeprodsq2  16749  pythagtriplem3  16758  pcdvdsb  16809  pcgcd1  16817  qexpz  16841  pockthg  16846  vdwnnlem1  16935  0ram  16960  ramz2  16964  lubss  18448  lubun  18450  clatleglb  18453  clatglbss  18454  mrelatglb  18495  isnsgrp  18660  issubmnd  18698  ress0g  18699  mhmvlin  18738  gsumccat  18778  frmdss2  18800  submefmnd  18832  mulgneg  19034  mulgdirlem  19047  submmulg  19060  subgmulg  19082  nmzsubg  19106  ghmmulg  19169  gsmsymgreqlem1  19371  pmtrfb  19406  psgnunilem4  19438  odmodnn0  19481  odnncl  19486  odmod  19487  odmulgid  19495  odmulgeq  19498  odf1o1  19513  odf1o2  19514  odngen  19518  gexdvdsi  19524  pgpfi1  19536  odcau  19545  subgslw  19557  fislw  19566  lsmssv  19584  lsmless1x  19585  lsmless2x  19586  lsmsubm  19594  lsmmod  19616  lsmmod2  19617  efgred  19689  cntzcmn  19781  ghmplusg  19787  odadd1  19789  odadd2  19790  odadd  19791  lsmcomx  19797  gsumconst  19875  ablsimpgprmd  20058  srg1zr  20162  ring1eq0  20245  mulgass2  20256  rngisom1  20414  rhmdvdsr  20453  isabvd  20757  rmodislmodlem  20892  rmodislmod  20893  lssintcl  20927  0lmhm  21004  lmhmvsca  21009  reslmhm2b  21018  pwssplit1  21023  pwssplit3  21025  lspfixed  21095  lspsnat  21112  rnglidlrng  21214  2idlcpblrng  21238  lidldvgen  21301  xrsdsreclblem  21379  regsumsupp  21589  obselocv  21695  uvcresum  21760  frlmsslsp  21763  frlmup4  21768  lindff1  21787  f1lindf  21789  lsslindf  21797  islindf4  21805  lbslcic  21808  issubassa  21834  evlsval2  22054  psrplusgpropd  22188  coe1subfv  22220  coe1mul2  22223  mpomatmul  22402  mamutpos  22414  scmatscmide  22463  mavmulsolcl  22507  marrepcl  22520  mdetdiag  22555  mdetunilem1  22568  mdetunilem3  22570  mdetunilem7  22574  mdetunilem9  22576  mdetmul  22579  slesolinvbi  22637  m2pmfzmap  22703  pmatcollpwlem  22736  pmatcollpw  22737  mp2pm2mplem4  22765  chpdmatlem3  22796  chfacfisfcpmat  22811  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  chfacfpmmulgsum2  22821  cayhamlem1  22822  cpmidpmatlem2  22827  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  riinopn  22864  neiint  23060  topssnei  23080  restntr  23138  iscnp4  23219  cnconst2  23239  cnrest2  23242  cnprest2  23246  cnpdis  23249  cnt0  23302  cnt1  23306  cnhaus  23310  ordthauslem  23339  cncmp  23348  fiuncmp  23360  sscmp  23361  hauscmp  23363  cnconn  23378  unconn  23385  nlly2i  23432  llynlly  23433  nllyidm  23445  finlocfin  23476  ptrescn  23595  xkococnlem  23615  qtopss  23671  kqfvima  23686  r0cld  23694  ordthmeolem  23757  fbssint  23794  fmf  23901  fmss  23902  elfm  23903  rnelfmlem  23908  rnelfm  23909  fmco  23917  flimss2  23928  flimss1  23929  flimrest  23939  flftg  23952  cnpflf2  23956  cnpflf  23957  flfcnp  23960  supnfcls  23976  fclsss1  23978  fclsss2  23979  fcfnei  23991  fcfelbas  23992  cnpfcfi  23996  subgntr  24063  opnsubg  24064  cldsubg  24067  ghmcnp  24071  utop2nei  24206  neipcfilu  24251  bldisj  24354  blgt0  24355  bl2in  24356  blss2ps  24359  blss2  24360  blssps  24380  blss  24381  xmetresbl  24393  lpbl  24459  blcld  24461  stdbdbl  24473  metcnp3  24496  metcnp2  24498  txmetcnp  24503  blval2  24518  nmoix  24685  nmoeq0  24692  icoopnst  24904  iocopnst  24905  xrhmeo  24912  nmhmcn  25088  cphsqrtcl2  25154  cphsqrtcl3  25155  cfil3i  25237  caublcls  25277  bcthlem5  25296  cmetcusp1  25321  cssbn  25343  rrxcph  25360  pjth  25407  ovoliunlem2  25472  volun  25514  volsup2  25574  mbfimaopn2  25626  iblconst  25787  itgconst  25788  dvcnp2  25889  dvcnp2OLD  25890  dvcn  25891  deg1mul3le  26090  deg1tmle  26091  dvdsq1p  26136  ig1peu  26148  ig1pdvds  26153  coeid3  26213  dgrmulc  26245  efcvx  26427  tanord  26515  logdivlti  26597  logccv  26640  recxpcl  26652  cxpeq  26735  ang180  26792  isosctrlem2  26797  cxp2lim  26955  amgm  26969  muval1  27111  dvdssqf  27116  mumullem2  27158  mumul  27159  bcmono  27256  lgsfcl2  27282  lgsdilem  27303  lgsdirprm  27310  lgsdir  27311  lgsdi  27313  lgsne0  27314  padicabv  27609  nosep1o  27661  nosep2o  27662  nosepssdm  27666  nolt02olem  27674  nosupres  27687  nosupbnd1lem1  27688  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  nosupbnd2  27696  noinfres  27702  noinfbnd1lem1  27703  noinfbnd1lem4  27706  noinfbnd1lem6  27708  noinfbnd2  27711  noetasuplem3  27715  noetalem1  27721  cutbdaybnd  27803  ltslpss  27916  leslss  27917  coinitslts  27927  addsass  28013  addsdi  28163  mulsass  28174  norecdiv  28198  bdayfinbndlem1  28475  z12bdaylem  28492  brbtwn2  28990  colinearalglem1  28991  colinearalg  28995  axcgrtr  29000  axsegconlem8  29009  axsegconlem9  29010  axsegconlem10  29011  axcontlem8  29056  axcontlem10  29058  elntg2  29070  vtxdlfuhgr1v  29565  umgr2wlk  30034  erclwwlksym  30108  clwwlkfo  30137  clwwlkext2edg  30143  erclwwlknsym  30157  clwwlknon1  30184  numclwwlk2lem1  30463  numclwwlk5  30475  frgrregord13  30483  nvmul0or  30737  ipval2lem2  30791  lnomul  30847  shless  31446  shlej1  31447  pjspansn  31664  hoadddi  31890  kbmul  32042  homco2  32064  kbass2  32204  eliccelico  32867  elicoelioo  32868  iocinioc2  32869  iocinif  32871  swrdrn2  33046  xrge0adddir  33110  xrge0npcan  33112  archiabl  33291  ress1r  33326  pidlnz  33468  grplsm0l  33495  intlidl  33512  ssmxidl  33566  pstmfval  34073  fmcncfil  34108  zrhnm  34144  qqhnm  34167  measvunilem  34389  volfiniune  34407  dya2iocnrect  34458  sibfinima  34516  probun  34596  probinc  34598  cndprob01  34612  signstfvp  34748  bnj517  35060  bnj594  35087  fissorduni  35265  pconnpi1  35450  cvmsss2  35487  mrsubcv  35723  msubvrs  35773  br6  35970  br4  35971  cgrcomim  36202  cgrtriv  36215  cgrextend  36221  segconeq  36223  btwntriv2  36225  btwnintr  36232  btwnexch3  36233  btwnouttr2  36235  trisegint  36241  cgrsub  36258  cgrxfr  36268  btwnxfr  36269  lineext  36289  btwnconn1lem13  36312  btwnconn1lem14  36313  btwnconn3  36316  segcon2  36318  brsegle  36321  brsegle2  36322  segletr  36327  segleantisym  36328  seglelin  36329  outsideofeu  36344  lineunray  36360  lineelsb2  36361  ivthALT  36548  weiunpo  36678  weiunso  36679  weiunfr  36680  weiunse  36681  lindsenlbs  37860  areacirc  37958  cocanfo  37964  upixp  37974  ismtyima  38048  rrndstprj2  38076  zerdivemp1x  38192  lsatfixedN  39379  lssat  39386  eqlkr  39469  eqlkr2  39470  lkrlsp  39472  lshpkrlem4  39483  opposet  39551  cvrcon3b  39647  cvrcmp  39653  atlen0  39680  atnle  39687  atlatmstc  39689  cvlatexch3  39708  cvlsupr2  39713  hlsupr2  39757  hlrelat2  39773  cvrexchlem  39789  lnnat  39797  atcvrj2b  39802  atle  39806  atexchcvrN  39810  atbtwn  39816  athgt  39826  3dimlem3  39831  3dim1  39837  1cvratlt  39844  1cvrjat  39845  ps-1  39847  ps-2  39848  3atlem3  39855  3atlem5  39857  3atlem7  39859  llni  39878  llni2  39882  atcvrlln2  39889  llnexatN  39891  llncmp  39892  2llnmat  39894  2at0mat0  39895  lplni  39902  lplnnle2at  39911  2atnelpln  39914  lplnllnneN  39926  llncvrlpln2  39927  2lplnmN  39929  2llnmj  39930  lplncmp  39932  lplnexatN  39933  lplnexllnN  39934  2llnm3N  39939  lvoli  39945  lvoli3  39947  islvol2aN  39962  4atlem0a  39963  4atlem3  39966  4atlem3a  39967  4atlem4a  39969  4atlem4b  39970  4atlem4c  39971  4atlem4d  39972  4atlem10b  39975  4atlem11  39979  4atlem12  39982  lplncvrlvol2  39985  lvolcmp  39987  2lplnmj  39992  islinei  40110  pmapglbx  40139  linepmap  40145  lneq2at  40148  lnjatN  40150  lncvrat  40152  lncmp  40153  2llnma3r  40158  elpaddatriN  40173  elpaddat  40174  paddcom  40183  paddss1  40187  paddss2  40188  paddss12  40189  paddasslem6  40195  paddasslem7  40196  paddasslem8  40197  paddasslem9  40198  paddasslem15  40204  pmodlem2  40217  pmodl42N  40221  pmapjoin  40222  llnmod1i2  40230  2polcon4bN  40288  polcon2bN  40290  poml4N  40323  poml6N  40325  osumcllem1N  40326  osumcllem2N  40327  osumcllem11N  40336  osumclN  40337  pmapojoinN  40338  pexmidlem2N  40341  pexmidlem3N  40342  pexmidlem4N  40343  pexmidlem6N  40345  pexmidlem7N  40346  pl42lem2N  40350  pl42lem3N  40351  pl42lem4N  40352  pl42N  40353  lhpexle2lem  40379  lhpexle3lem  40381  lhpexle3  40382  lhpmcvr3  40395  lhp2at0nle  40405  lhprelat3N  40410  4atex  40446  4atex2  40447  lauteq  40465  lautco  40467  ltrncoidN  40498  ltrneq2  40518  ltrnnidn  40544  ltrnideq  40545  trlnid  40549  ltrnatlw  40553  trlnle  40556  trlval3  40557  trlval4  40558  cdlemc  40567  cdlemd5  40572  cdlemd9  40576  ltrneq3  40578  cdleme0moN  40595  cdleme20  40694  cdleme21j  40706  cdleme21  40707  cdleme27cl  40736  cdlemefrs29bpre0  40766  cdlemefs27cl  40783  cdlemefs32sn1aw  40784  cdleme43fsv1snlem  40790  cdleme32d  40814  cdleme32f  40816  cdleme32le  40817  cdleme35h2  40827  cdleme38n  40834  cdleme40m  40837  cdleme41snaw  40846  cdleme42ke  40855  cdleme17d3  40866  cdleme48fvg  40870  cdlemeg46fvcl  40876  cdlemeg46fgN  40904  cdleme48gfv1  40906  cdleme48fgv  40908  cdleme50trn3  40923  trlord  40939  ltrniotavalbN  40954  cdlemb3  40976  cdlemg6c  40990  cdlemg6  40993  cdlemg7N  40996  cdlemg8c  40999  cdlemg8  41001  cdlemg11a  41007  cdlemg11b  41012  cdlemg12e  41017  cdlemg15a  41025  cdlemg15  41026  cdlemg16  41027  cdlemg16z  41029  cdlemg16zz  41030  cdlemg17dN  41033  cdlemg18a  41048  cdlemg20  41055  cdlemg22  41057  cdlemg24  41058  cdlemg37  41059  cdlemg31d  41070  cdlemg29  41075  cdlemg33b  41077  cdlemg33  41081  cdlemg38  41085  cdlemg39  41086  cdlemg40  41087  trlco  41097  trlcone  41098  cdlemg42  41099  cdlemg44b  41102  ltrncom  41108  trljco  41110  tendococl  41142  tendoplcl  41151  tendoplcom  41152  cdlemj2  41192  cdlemj3  41193  tendoid0  41195  tendoconid  41199  tendotr  41200  cdlemk25-3  41274  cdlemk26b-3  41275  cdlemk34  41280  cdlemk36  41283  cdlemk38  41285  cdlemkid4  41304  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk19x  41313  cdlemk53  41327  cdlemk55  41331  cdlemk55u  41336  cdlemk39u  41338  cdlemk19u  41340  cdlemk56  41341  tendoex  41345  cdleml3N  41348  cdleml5N  41350  tendospcanN  41393  cdlemm10N  41488  cdlemn11pre  41580  dihord2pre  41595  dihvalcqpre  41605  dihopelvalcpre  41618  dihord6apre  41626  dihord5b  41629  dihord5apre  41632  dihord  41634  dihmeetlem1N  41660  dihglblem5apreN  41661  dihglblem3N  41665  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetbN  41673  dihmeetlem4preN  41676  dihmeetlem5  41678  dihmeetlem7N  41680  dihmeetlem10N  41686  dihmeetlem11N  41687  dihmeetlem12N  41688  dihmeetlem13N  41689  dihmeetlem15N  41691  dihmeetlem16N  41692  dihmeetlem17N  41693  dihmeetlem18N  41694  dihmeetlem19N  41695  dihmeetALTN  41697  dih1dimatlem0  41698  dihlspsnssN  41702  dihlspsnat  41703  mapdh8ad  42149  hdmap14lem14  42251  hgmapvvlem3  42295  aks6d1c6isolem1  42538  dvdsexpnn  42697  resubcan2  42752  mzprename  43100  eldioph2lem1  43111  lzunuz  43119  rencldnfi  43172  pellexlem2  43181  infmrgelbi  43229  pellfundglb  43236  pellfund14gap  43238  qirropth  43259  rmxycomplete  43268  congadd  43317  acongeq  43334  jm2.19  43344  jm2.23  43347  jm2.20nn  43348  jm2.27  43359  jm3.1  43371  aomclem6  43410  lnmepi  43436  lmhmfgsplit  43437  lmhmlnmsplit  43438  pwssplit4  43440  hbtlem2  43475  hbtlem5  43479  dgraa0p  43500  proot1hash  43546  iocunico  43562  oasubex  43637  oege1  43657  relexpxpmin  44067  brtrclfv2  44077  ntrclsiso  44417  ntrclskb  44419  ntrclsk3  44420  k0004lem3  44499  grur1cld  44582  ismnu  44611  grumnudlem  44635  suprnmpt  45527  wessf1ornlem  45538  projf1o  45549  snunioo1  45866  iccintsng  45877  lptre2pt  45992  limcleqr  45996  fnlimfvre  46026  limsupgtlem  46129  volioc  46324  iblspltprt  46325  stoweidlem19  46371  stoweidlem20  46372  stoweidlem22  46374  stoweidlem28  46380  stoweidlem34  46386  stoweidlem44  46396  stoweidlem60  46412  wallispilem3  46419  fourierdlem41  46500  fourierdlem42  46501  fourierdlem49  46507  fourierdlem51  46509  fourierdlem54  46512  fourierdlem74  46532  fourierdlem97  46555  caratheodorylem2  46879  ovnsubaddlem2  46923  hspmbllem2  46979  smflimmpt  47162  smflimsupmpt  47181  smfliminfmpt  47184  funfocofob  47432  fzopredsuc  47677  imasetpreimafvbijlemfv  47756  iccpartigtl  47777  lighneal  47965  oexpnegALTV  48031  oexpnegnz  48032  tgblthelfgott  48169  clnbgrgrim  48288  uhgrimgrlim  48341  gpgusgralem  48410  lidldomn1  48585  ofaddmndmap  48697  lincdifsn  48778  lincellss  48780  lincresunit3lem3  48828  islindeps2  48837  lindssnlvec  48840  fdivmptf  48895  refdivmptf  48896  rrx2linest  49096  itsclc0yqsollem1  49116  itsclc0b  49126  itsclquadb  49130  itscnhlinecirc02plem3  49138  diag1  49657  setc1onsubc  49955