Theorem simpl1 1191

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 1185	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  1248  simpl21  1251  simpl31  1254  simp1l1  1266  simp2l1  1272  simp3l1  1278  3anandirs  1472  rspc3ev  3652  2nreu  4467  predtrss  6354  frpomin  6372  f1prex  7320  cocan1  7327  weniso  7390  frrlem4  8330  frrlem10  8336  fprlem1  8341  smogt  8423  smocdmdom  8424  omeulem1  8638  nnmord  8688  nnmword  8689  naddasslem1  8750  naddasslem2  8751  difsnen  9119  enfixsn  9147  mapunen  9212  ac6sfi  9348  fipreima  9428  elfiun  9499  ordiso2  9584  wemaplem2  9616  en2eqpr  10076  indcardi  10110  fodomfi2  10129  iunfictbso  10183  infmap2  10286  cofsmo  10338  cfsmolem  10339  coftr  10342  fin23lem11  10386  fincssdom  10392  fin23lem26  10394  isf32lem9  10430  ac6num  10548  gchdomtri  10698  gchpwdom  10739  winainflem  10762  tskuni  10852  gruima  10871  gruf  10880  grudomon  10886  elnpi  11057  distrlem4pr  11095  prlem934  11102  addcan  11474  addcan2  11475  divmulass  11972  divmulasscom  11973  ltmul1a  12143  suprleub  12261  supmul1  12264  suprzcl  12723  uzsupss  13005  xleadd1a  13315  xlesubadd  13325  xmulasslem3  13348  xlemul2a  13351  xadddilem  13356  xadddi2  13359  ixxun  13423  icoshftf1o  13534  ioounsn  13537  snunioc  13540  lincmb01cmp  13555  iccf1o  13556  nn0p1elfzo  13759  fzofzim  13763  fzoopth  13812  ltexp2a  14216  leexp2  14221  ltexp2r  14223  exple1  14226  expnlbnd2  14283  fun2dmnop0  14553  ccatass  14636  swrdswrdlem  14752  ccatopth  14764  repswpfx  14833  2cshw  14861  cshimadifsn  14878  cshimadifsn0  14879  cshco  14885  repsco  14889  s2f1o  14965  limsupgre  15527  addcn2  15640  mulcn2  15642  ntrivcvgmul  15950  binomrisefac  16090  dvdsmodexp  16310  dvdsadd2b  16354  dvdsexp2im  16375  dvdsmod  16377  oexpneg  16393  sadass  16517  gcdass  16594  rplpwr  16605  lcmfunsnlem1  16684  coprmdvds2  16701  rpmulgcd2  16703  qredeq  16704  rpdvds  16707  cncongr2  16715  rpexp  16769  prmdiveq  16833  hashgcdlem  16835  odzdvds  16842  modprmn0modprm0  16854  coprimeprodsq2  16856  pythagtriplem3  16865  pcdvdsb  16916  pcgcd1  16924  qexpz  16948  pockthg  16953  vdwnnlem1  17042  0ram  17067  ramz2  17071  lubss  18583  lubun  18585  clatleglb  18588  clatglbss  18589  mrelatglb  18630  isnsgrp  18761  issubmnd  18799  ress0g  18800  mhmvlin  18836  gsumccat  18876  frmdss2  18898  submefmnd  18930  mulgneg  19132  mulgdirlem  19145  submmulg  19158  subgmulg  19180  nmzsubg  19205  ghmmulg  19268  gsmsymgreqlem1  19472  pmtrfb  19507  psgnunilem4  19539  odmodnn0  19582  odnncl  19587  odmod  19588  odmulgid  19596  odmulgeq  19599  odf1o1  19614  odf1o2  19615  odngen  19619  gexdvdsi  19625  pgpfi1  19637  odcau  19646  subgslw  19658  fislw  19667  lsmssv  19685  lsmless1x  19686  lsmless2x  19687  lsmsubm  19695  lsmmod  19717  lsmmod2  19718  efgred  19790  cntzcmn  19882  ghmplusg  19888  odadd1  19890  odadd2  19891  odadd  19892  lsmcomx  19898  gsumconst  19976  ablsimpgprmd  20159  srg1zr  20242  ring1eq0  20321  mulgass2  20332  rngisom1  20492  rhmdvdsr  20534  isabvd  20835  rmodislmodlem  20949  rmodislmod  20950  rmodislmodOLD  20951  lssintcl  20985  0lmhm  21062  lmhmvsca  21067  reslmhm2b  21076  pwssplit1  21081  pwssplit3  21083  lspfixed  21153  lspsnat  21170  rnglidlrng  21280  2idlcpblrng  21304  lidldvgen  21367  xrsdsreclblem  21453  regsumsupp  21663  obselocv  21771  uvcresum  21836  frlmsslsp  21839  frlmup4  21844  lindff1  21863  f1lindf  21865  lsslindf  21873  islindf4  21881  lbslcic  21884  issubassa  21910  evlsval2  22134  psrplusgpropd  22258  coe1subfv  22290  coe1mul2  22293  mpomatmul  22473  mamutpos  22485  scmatscmide  22534  mavmulsolcl  22578  marrepcl  22591  mdetdiag  22626  mdetunilem1  22639  mdetunilem3  22641  mdetunilem7  22645  mdetunilem9  22647  mdetmul  22650  slesolinvbi  22708  m2pmfzmap  22774  pmatcollpwlem  22807  pmatcollpw  22808  mp2pm2mplem4  22836  chpdmatlem3  22867  chfacfisfcpmat  22882  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  chfacfpmmulgsum2  22892  cayhamlem1  22893  cpmidpmatlem2  22898  cpmadugsumlemB  22901  cpmadugsumlemC  22902  cpmadugsumlemF  22903  riinopn  22935  neiint  23133  topssnei  23153  restntr  23211  iscnp4  23292  cnconst2  23312  cnrest2  23315  cnprest2  23319  cnpdis  23322  cnt0  23375  cnt1  23379  cnhaus  23383  ordthauslem  23412  cncmp  23421  fiuncmp  23433  sscmp  23434  hauscmp  23436  cnconn  23451  unconn  23458  nlly2i  23505  llynlly  23506  nllyidm  23518  finlocfin  23549  ptrescn  23668  xkococnlem  23688  qtopss  23744  kqfvima  23759  r0cld  23767  ordthmeolem  23830  fbssint  23867  fmf  23974  fmss  23975  elfm  23976  rnelfmlem  23981  rnelfm  23982  fmco  23990  flimss2  24001  flimss1  24002  flimrest  24012  flftg  24025  cnpflf2  24029  cnpflf  24030  flfcnp  24033  supnfcls  24049  fclsss1  24051  fclsss2  24052  fcfnei  24064  fcfelbas  24065  cnpfcfi  24069  subgntr  24136  opnsubg  24137  cldsubg  24140  ghmcnp  24144  utop2nei  24280  neipcfilu  24326  bldisj  24429  blgt0  24430  bl2in  24431  blss2ps  24434  blss2  24435  blssps  24455  blss  24456  xmetresbl  24468  lpbl  24537  blcld  24539  stdbdbl  24551  metcnp3  24574  metcnp2  24576  txmetcnp  24581  blval2  24596  nmoix  24771  nmoeq0  24778  icoopnst  24988  iocopnst  24989  xrhmeo  24996  nmhmcn  25172  cphsqrtcl2  25239  cphsqrtcl3  25240  cfil3i  25322  caublcls  25362  bcthlem5  25381  cmetcusp1  25406  cssbn  25428  rrxcph  25445  pjth  25492  ovoliunlem2  25557  volun  25599  volsup2  25659  mbfimaopn2  25711  iblconst  25873  itgconst  25874  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  deg1mul3le  26176  deg1tmle  26177  dvdsq1p  26222  ig1peu  26234  ig1pdvds  26239  coeid3  26299  dgrmulc  26331  efcvx  26511  tanord  26598  logdivlti  26680  logccv  26723  recxpcl  26735  cxpeq  26818  ang180  26875  isosctrlem2  26880  cxp2lim  27038  amgm  27052  muval1  27194  dvdssqf  27199  mumullem2  27241  mumul  27242  bcmono  27339  lgsfcl2  27365  lgsdilem  27386  lgsdirprm  27393  lgsdir  27394  lgsdi  27396  lgsne0  27397  padicabv  27692  nosep1o  27744  nosep2o  27745  nosepssdm  27749  nolt02olem  27757  nosupres  27770  nosupbnd1lem1  27771  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  nosupbnd2  27779  noinfres  27785  noinfbnd1lem1  27786  noinfbnd1lem4  27789  noinfbnd1lem6  27791  noinfbnd2  27794  noetasuplem3  27798  noetalem1  27804  scutbdaybnd  27878  sltlpss  27963  slelss  27964  coinitsslt  27971  addsass  28056  addsdi  28199  mulsass  28210  norecdiv  28234  brbtwn2  28938  colinearalglem1  28939  colinearalg  28943  axcgrtr  28948  axsegconlem8  28957  axsegconlem9  28958  axsegconlem10  28959  axcontlem8  29004  axcontlem10  29006  elntg2  29018  vtxdlfuhgr1v  29515  umgr2wlk  29982  erclwwlksym  30053  clwwlkfo  30082  clwwlkext2edg  30088  erclwwlknsym  30102  clwwlknon1  30129  numclwwlk2lem1  30408  numclwwlk5  30420  frgrregord13  30428  nvmul0or  30682  ipval2lem2  30736  lnomul  30792  shless  31391  shlej1  31392  pjspansn  31609  hoadddi  31835  kbmul  31987  homco2  32009  kbass2  32149  eliccelico  32782  elicoelioo  32783  iocinioc2  32784  iocinif  32786  swrdrn2  32921  xrge0adddir  33004  xrge0npcan  33006  archiabl  33178  ress1r  33214  pidlnz  33369  grplsm0l  33396  intlidl  33413  ssmxidl  33467  pstmfval  33842  fmcncfil  33877  zrhnm  33915  qqhnm  33936  measvunilem  34176  volfiniune  34194  dya2iocnrect  34246  sibfinima  34304  probun  34384  probinc  34386  cndprob01  34400  signstfvp  34548  bnj517  34861  bnj594  34888  pconnpi1  35205  cvmsss2  35242  mrsubcv  35478  msubvrs  35528  br6  35719  br4  35720  cgrcomim  35953  cgrtriv  35966  cgrextend  35972  segconeq  35974  btwntriv2  35976  btwnintr  35983  btwnexch3  35984  btwnouttr2  35986  trisegint  35992  cgrsub  36009  cgrxfr  36019  btwnxfr  36020  lineext  36040  btwnconn1lem13  36063  btwnconn1lem14  36064  btwnconn3  36067  segcon2  36069  brsegle  36072  brsegle2  36073  segletr  36078  segleantisym  36079  seglelin  36080  outsideofeu  36095  lineunray  36111  lineelsb2  36112  ivthALT  36301  weiunpo  36431  weiunso  36432  weiunfr  36433  weiunse  36434  lindsenlbs  37575  areacirc  37673  cocanfo  37679  upixp  37689  ismtyima  37763  rrndstprj2  37791  zerdivemp1x  37907  lsatfixedN  38965  lssat  38972  eqlkr  39055  eqlkr2  39056  lkrlsp  39058  lshpkrlem4  39069  opposet  39137  cvrcon3b  39233  cvrcmp  39239  atlen0  39266  atnle  39273  atlatmstc  39275  cvlatexch3  39294  cvlsupr2  39299  hlsupr2  39344  hlrelat2  39360  cvrexchlem  39376  lnnat  39384  atcvrj2b  39389  atle  39393  atexchcvrN  39397  atbtwn  39403  athgt  39413  3dimlem3  39418  3dim1  39424  1cvratlt  39431  1cvrjat  39432  ps-1  39434  ps-2  39435  3atlem3  39442  3atlem5  39444  3atlem7  39446  llni  39465  llni2  39469  atcvrlln2  39476  llnexatN  39478  llncmp  39479  2llnmat  39481  2at0mat0  39482  lplni  39489  lplnnle2at  39498  2atnelpln  39501  lplnllnneN  39513  llncvrlpln2  39514  2lplnmN  39516  2llnmj  39517  lplncmp  39519  lplnexatN  39520  lplnexllnN  39521  2llnm3N  39526  lvoli  39532  lvoli3  39534  islvol2aN  39549  4atlem0a  39550  4atlem3  39553  4atlem3a  39554  4atlem4a  39556  4atlem4b  39557  4atlem4c  39558  4atlem4d  39559  4atlem10b  39562  4atlem11  39566  4atlem12  39569  lplncvrlvol2  39572  lvolcmp  39574  2lplnmj  39579  islinei  39697  pmapglbx  39726  linepmap  39732  lneq2at  39735  lnjatN  39737  lncvrat  39739  lncmp  39740  2llnma3r  39745  elpaddatriN  39760  elpaddat  39761  paddcom  39770  paddss1  39774  paddss2  39775  paddss12  39776  paddasslem6  39782  paddasslem7  39783  paddasslem8  39784  paddasslem9  39785  paddasslem15  39791  pmodlem2  39804  pmodl42N  39808  pmapjoin  39809  llnmod1i2  39817  2polcon4bN  39875  polcon2bN  39877  poml4N  39910  poml6N  39912  osumcllem1N  39913  osumcllem2N  39914  osumcllem11N  39923  osumclN  39924  pmapojoinN  39925  pexmidlem2N  39928  pexmidlem3N  39929  pexmidlem4N  39930  pexmidlem6N  39932  pexmidlem7N  39933  pl42lem2N  39937  pl42lem3N  39938  pl42lem4N  39939  pl42N  39940  lhpexle2lem  39966  lhpexle3lem  39968  lhpexle3  39969  lhpmcvr3  39982  lhp2at0nle  39992  lhprelat3N  39997  4atex  40033  4atex2  40034  lauteq  40052  lautco  40054  ltrncoidN  40085  ltrneq2  40105  ltrnnidn  40131  ltrnideq  40132  trlnid  40136  ltrnatlw  40140  trlnle  40143  trlval3  40144  trlval4  40145  cdlemc  40154  cdlemd5  40159  cdlemd9  40163  ltrneq3  40165  cdleme0moN  40182  cdleme20  40281  cdleme21j  40293  cdleme21  40294  cdleme27cl  40323  cdlemefrs29bpre0  40353  cdlemefs27cl  40370  cdlemefs32sn1aw  40371  cdleme43fsv1snlem  40377  cdleme32d  40401  cdleme32f  40403  cdleme32le  40404  cdleme35h2  40414  cdleme38n  40421  cdleme40m  40424  cdleme41snaw  40433  cdleme42ke  40442  cdleme17d3  40453  cdleme48fvg  40457  cdlemeg46fvcl  40463  cdlemeg46fgN  40491  cdleme48gfv1  40493  cdleme48fgv  40495  cdleme50trn3  40510  trlord  40526  ltrniotavalbN  40541  cdlemb3  40563  cdlemg6c  40577  cdlemg6  40580  cdlemg7N  40583  cdlemg8c  40586  cdlemg8  40588  cdlemg11a  40594  cdlemg11b  40599  cdlemg12e  40604  cdlemg15a  40612  cdlemg15  40613  cdlemg16  40614  cdlemg16z  40616  cdlemg16zz  40617  cdlemg17dN  40620  cdlemg18a  40635  cdlemg20  40642  cdlemg22  40644  cdlemg24  40645  cdlemg37  40646  cdlemg31d  40657  cdlemg29  40662  cdlemg33b  40664  cdlemg33  40668  cdlemg38  40672  cdlemg39  40673  cdlemg40  40674  trlco  40684  trlcone  40685  cdlemg42  40686  cdlemg44b  40689  ltrncom  40695  trljco  40697  tendococl  40729  tendoplcl  40738  tendoplcom  40739  cdlemj2  40779  cdlemj3  40780  tendoid0  40782  tendoconid  40786  tendotr  40787  cdlemk25-3  40861  cdlemk26b-3  40862  cdlemk34  40867  cdlemk36  40870  cdlemk38  40872  cdlemkid4  40891  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk19x  40900  cdlemk53  40914  cdlemk55  40918  cdlemk55u  40923  cdlemk39u  40925  cdlemk19u  40927  cdlemk56  40928  tendoex  40932  cdleml3N  40935  cdleml5N  40937  tendospcanN  40980  cdlemm10N  41075  cdlemn11pre  41167  dihord2pre  41182  dihvalcqpre  41192  dihopelvalcpre  41205  dihord6apre  41213  dihord5b  41216  dihord5apre  41219  dihord  41221  dihmeetlem1N  41247  dihglblem5apreN  41248  dihglblem3N  41252  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetbN  41260  dihmeetlem4preN  41263  dihmeetlem5  41265  dihmeetlem7N  41267  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem12N  41275  dihmeetlem13N  41276  dihmeetlem15N  41278  dihmeetlem16N  41279  dihmeetlem17N  41280  dihmeetlem18N  41281  dihmeetlem19N  41282  dihmeetALTN  41284  dih1dimatlem0  41285  dihlspsnssN  41289  dihlspsnat  41290  mapdh8ad  41736  hdmap14lem14  41838  hgmapvvlem3  41882  aks6d1c6isolem1  42131  dvdsexpnn  42320  resubcan2  42364  mzprename  42705  eldioph2lem1  42716  lzunuz  42724  rencldnfi  42777  pellexlem2  42786  infmrgelbi  42834  pellfundglb  42841  pellfund14gap  42843  qirropth  42864  rmxycomplete  42874  congadd  42923  acongeq  42940  jm2.19  42950  jm2.23  42953  jm2.20nn  42954  jm2.27  42965  jm3.1  42977  aomclem6  43016  lnmepi  43042  lmhmfgsplit  43043  lmhmlnmsplit  43044  pwssplit4  43046  hbtlem2  43081  hbtlem5  43085  dgraa0p  43106  proot1hash  43156  iocunico  43172  oasubex  43248  oege1  43268  relexpxpmin  43679  brtrclfv2  43689  ntrclsiso  44029  ntrclskb  44031  ntrclsk3  44032  k0004lem3  44111  grur1cld  44201  ismnu  44230  grumnudlem  44254  suprnmpt  45081  wessf1ornlem  45092  projf1o  45104  snunioo1  45430  iccintsng  45441  lptre2pt  45561  limcleqr  45565  fnlimfvre  45595  limsupgtlem  45698  volioc  45893  iblspltprt  45894  stoweidlem19  45940  stoweidlem20  45941  stoweidlem22  45943  stoweidlem28  45949  stoweidlem34  45955  stoweidlem44  45965  stoweidlem60  45981  wallispilem3  45988  fourierdlem41  46069  fourierdlem42  46070  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem74  46101  fourierdlem97  46124  caratheodorylem2  46448  ovnsubaddlem2  46492  hspmbllem2  46548  smflimmpt  46731  smflimsupmpt  46750  smfliminfmpt  46753  funfocofob  46993  fzopredsuc  47238  imasetpreimafvbijlemfv  47276  iccpartigtl  47297  lighneal  47485  oexpnegALTV  47551  oexpnegnz  47552  tgblthelfgott  47689  clnbgrgrim  47786  uhgrimgrlim  47811  lidldomn1  47954  ofaddmndmap  48068  lincdifsn  48153  lincellss  48155  lincresunit3lem3  48203  islindeps2  48212  lindssnlvec  48215  fdivmptf  48275  refdivmptf  48276  rrx2linest  48476  itsclc0yqsollem1  48496  itsclc0b  48506  itsclquadb  48510  itscnhlinecirc02plem3  48518