Theorem simpl1 1198

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpl11  1255  simpl21  1258  simpl31  1261  simp1l1  1273  simp2l1  1279  simp3l1  1285  3anandirs  1480  rspc3ev  3584  2nreu  4379  predtrss  6280  frpomin  6298  f1prex  7235  cocan1  7242  weniso  7305  frrlem4  8236  frrlem10  8242  fprlem1  8247  smogt  8304  smocdmdom  8305  omeulem1  8514  nnmord  8565  nnmword  8566  naddasslem1  8627  naddasslem2  8628  difsnen  8994  enfixsn  9021  mapunen  9081  ac6sfi  9191  fipreima  9265  elfiun  9340  ordiso2  9427  wemaplem2  9459  en2eqpr  9927  indcardi  9961  fodomfi2  9980  iunfictbso  10034  infmap2  10137  cofsmo  10189  cfsmolem  10190  coftr  10193  fin23lem11  10237  fincssdom  10243  fin23lem26  10245  isf32lem9  10281  ac6num  10399  gchdomtri  10550  gchpwdom  10591  winainflem  10614  tskuni  10704  gruima  10723  gruf  10732  grudomon  10738  elnpi  10909  distrlem4pr  10947  prlem934  10954  addcan  11328  addcan2  11329  divmulass  11830  divmulasscom  11831  ltmul1a  12002  suprleub  12120  supmul1  12123  suprzcl  12607  uzsupss  12888  xleadd1a  13203  xlesubadd  13213  xmulasslem3  13236  xlemul2a  13239  xadddilem  13244  xadddi2  13247  ixxun  13312  icoshftf1o  13425  ioounsn  13428  snunioc  13431  lincmb01cmp  13446  iccf1o  13447  nn0p1elfzo  13655  fzofzim  13662  fzoopth  13715  ltexp2a  14126  leexp2  14131  ltexp2r  14133  exple1  14137  expnlbnd2  14194  fun2dmnop0  14464  ccatass  14549  swrdswrdlem  14664  ccatopth  14676  repswpfx  14745  2cshw  14773  cshimadifsn  14789  cshimadifsn0  14790  cshco  14796  repsco  14800  s2f1o  14876  limsupgre  15441  addcn2  15554  mulcn2  15556  ntrivcvgmul  15865  binomrisefac  16005  dvdsmodexp  16227  dvdsadd2b  16273  dvdsexp2im  16294  dvdsmod  16296  oexpneg  16312  sadass  16438  gcdass  16514  rplpwr  16525  lcmfunsnlem1  16604  coprmdvds2  16621  rpmulgcd2  16623  qredeq  16624  rpdvds  16627  cncongr2  16635  rpexp  16690  prmdiveq  16754  hashgcdlem  16756  odzdvds  16764  modprmn0modprm0  16776  coprimeprodsq2  16778  pythagtriplem3  16787  pcdvdsb  16838  pcgcd1  16846  qexpz  16870  pockthg  16875  vdwnnlem1  16964  0ram  16989  ramz2  16993  lubss  18477  lubun  18479  clatleglb  18482  clatglbss  18483  mrelatglb  18524  isnsgrp  18689  issubmnd  18727  ress0g  18728  mhmvlin  18767  gsumccat  18807  frmdss2  18829  submefmnd  18861  mulgneg  19066  mulgdirlem  19079  submmulg  19092  subgmulg  19114  nmzsubg  19138  ghmmulg  19201  gsmsymgreqlem1  19403  pmtrfb  19438  psgnunilem4  19470  odmodnn0  19513  odnncl  19518  odmod  19519  odmulgid  19527  odmulgeq  19530  odf1o1  19545  odf1o2  19546  odngen  19550  gexdvdsi  19556  pgpfi1  19568  odcau  19577  subgslw  19589  fislw  19598  lsmssv  19616  lsmless1x  19617  lsmless2x  19618  lsmsubm  19626  lsmmod  19648  lsmmod2  19649  efgred  19721  cntzcmn  19813  ghmplusg  19819  odadd1  19821  odadd2  19822  odadd  19823  lsmcomx  19829  gsumconst  19907  ablsimpgprmd  20090  srg1zr  20194  ring1eq0  20277  mulgass2  20288  rngisom1  20444  rhmdvdsr  20487  isabvd  20791  rmodislmodlem  20926  rmodislmod  20927  lssintcl  20961  0lmhm  21037  lmhmvsca  21042  reslmhm2b  21051  pwssplit1  21056  pwssplit3  21058  lspfixed  21128  lspsnat  21145  rnglidlrng  21247  2idlcpblrng  21271  lidldvgen  21334  xrsdsreclblem  21395  regsumsupp  21604  obselocv  21710  uvcresum  21775  frlmsslsp  21778  frlmup4  21783  lindff1  21802  f1lindf  21804  lsslindf  21812  islindf4  21820  lbslcic  21823  issubassa  21849  evlsval2  22070  psrplusgpropd  22227  coe1subfv  22259  coe1mul2  22262  mpomatmul  22436  mamutpos  22448  scmatscmide  22497  mavmulsolcl  22541  marrepcl  22554  mdetdiag  22589  mdetunilem1  22602  mdetunilem3  22604  mdetunilem7  22608  mdetunilem9  22610  mdetmul  22613  slesolinvbi  22671  m2pmfzmap  22737  pmatcollpwlem  22770  pmatcollpw  22771  mp2pm2mplem4  22799  chpdmatlem3  22830  chfacfisfcpmat  22845  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  chfacfpmmulgsum2  22855  cayhamlem1  22856  cpmidpmatlem2  22861  cpmadugsumlemB  22864  cpmadugsumlemC  22865  cpmadugsumlemF  22866  riinopn  22898  neiint  23094  topssnei  23114  restntr  23172  iscnp4  23253  cnconst2  23273  cnrest2  23276  cnprest2  23280  cnpdis  23283  cnt0  23336  cnt1  23340  cnhaus  23344  ordthauslem  23373  cncmp  23382  fiuncmp  23394  sscmp  23395  hauscmp  23397  cnconn  23412  unconn  23419  nlly2i  23466  llynlly  23467  nllyidm  23479  finlocfin  23510  ptrescn  23629  xkococnlem  23649  qtopss  23705  kqfvima  23720  r0cld  23728  ordthmeolem  23791  fbssint  23828  fmf  23935  fmss  23936  elfm  23937  rnelfmlem  23942  rnelfm  23943  fmco  23951  flimss2  23962  flimss1  23963  flimrest  23973  flftg  23986  cnpflf2  23990  cnpflf  23991  flfcnp  23994  supnfcls  24010  fclsss1  24012  fclsss2  24013  fcfnei  24025  fcfelbas  24026  cnpfcfi  24030  subgntr  24097  opnsubg  24098  cldsubg  24101  ghmcnp  24105  utop2nei  24240  neipcfilu  24285  bldisj  24388  blgt0  24389  bl2in  24390  blss2ps  24393  blss2  24394  blssps  24414  blss  24415  xmetresbl  24427  lpbl  24493  blcld  24495  stdbdbl  24507  metcnp3  24530  metcnp2  24532  txmetcnp  24537  blval2  24552  nmoix  24719  nmoeq0  24726  icoopnst  24931  iocopnst  24932  xrhmeo  24938  nmhmcn  25112  cphsqrtcl2  25178  cphsqrtcl3  25179  cfil3i  25261  caublcls  25301  bcthlem5  25320  cmetcusp1  25345  cssbn  25367  rrxcph  25384  pjth  25431  ovoliunlem2  25495  volun  25537  volsup2  25597  mbfimaopn2  25649  iblconst  25810  itgconst  25811  dvcnp2  25912  dvcn  25913  deg1mul3le  26107  deg1tmle  26108  dvdsq1p  26153  ig1peu  26165  ig1pdvds  26170  coeid3  26230  dgrmulc  26261  efcvx  26439  tanord  26527  logdivlti  26609  logccv  26652  recxpcl  26664  cxpeq  26746  ang180  26803  isosctrlem2  26808  cxp2lim  26965  amgm  26979  muval1  27121  dvdssqf  27126  mumullem2  27168  mumul  27169  bcmono  27265  lgsfcl2  27291  lgsdilem  27312  lgsdirprm  27319  lgsdir  27320  lgsdi  27322  lgsne0  27323  padicabv  27618  nosep1o  27670  nosep2o  27671  nosepssdm  27675  nolt02olem  27683  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  nosupbnd2  27705  noinfres  27711  noinfbnd1lem1  27712  noinfbnd1lem4  27715  noinfbnd1lem6  27717  noinfbnd2  27720  noetasuplem3  27724  noetalem1  27730  cutbdaybnd  27812  ltslpss  27925  leslss  27926  coinitslts  27936  addsass  28022  addsdi  28172  mulsass  28183  norecdiv  28207  bdayfinbndlem1  28484  z12bdaylem  28501  brbtwn2  28999  colinearalglem1  29000  colinearalg  29004  axcgrtr  29009  axsegconlem8  29018  axsegconlem9  29019  axsegconlem10  29020  axcontlem8  29065  axcontlem10  29067  elntg2  29079  vtxdlfuhgr1v  29573  umgr2wlk  30042  erclwwlksym  30116  clwwlkfo  30145  clwwlkext2edg  30151  erclwwlknsym  30165  clwwlknon1  30192  numclwwlk2lem1  30471  numclwwlk5  30483  frgrregord13  30491  nvmul0or  30746  ipval2lem2  30800  lnomul  30856  shless  31455  shlej1  31456  pjspansn  31673  hoadddi  31899  kbmul  32051  homco2  32073  kbass2  32213  eliccelico  32876  elicoelioo  32877  iocinioc2  32878  iocinif  32880  swrdrn2  33040  xrge0adddir  33104  xrge0npcan  33106  archiabl  33286  ress1r  33321  pidlnz  33466  grplsm0l  33493  intlidl  33510  ssmxidl  33564  pstmfval  34087  fmcncfil  34122  zrhnm  34158  qqhnm  34181  measvunilem  34403  volfiniune  34421  dya2iocnrect  34472  sibfinima  34530  probun  34610  probinc  34612  cndprob01  34626  signstfvp  34762  bnj517  35074  bnj594  35101  fissorduni  35278  pconnpi1  35472  cvmsss2  35509  mrsubcv  35745  msubvrs  35795  br6  35992  br4  35993  cgrcomim  36224  cgrtriv  36237  cgrextend  36243  segconeq  36245  btwntriv2  36247  btwnintr  36254  btwnexch3  36255  btwnouttr2  36257  trisegint  36263  cgrsub  36280  cgrxfr  36290  btwnxfr  36291  lineext  36311  btwnconn1lem13  36334  btwnconn1lem14  36335  btwnconn3  36338  segcon2  36340  brsegle  36343  brsegle2  36344  segletr  36349  segleantisym  36350  seglelin  36351  outsideofeu  36366  lineunray  36382  lineelsb2  36383  ivthALT  36570  weiunpo  36700  weiunso  36701  weiunfr  36702  weiunse  36703  lindsenlbs  37989  areacirc  38087  cocanfo  38093  upixp  38103  ismtyima  38177  rrndstprj2  38205  zerdivemp1x  38321  lsatfixedN  39508  lssat  39515  eqlkr  39598  eqlkr2  39599  lkrlsp  39601  lshpkrlem4  39612  opposet  39680  cvrcon3b  39776  cvrcmp  39782  atlen0  39809  atnle  39816  atlatmstc  39818  cvlatexch3  39837  cvlsupr2  39842  hlsupr2  39886  hlrelat2  39902  cvrexchlem  39918  lnnat  39926  atcvrj2b  39931  atle  39935  atexchcvrN  39939  atbtwn  39945  athgt  39955  3dimlem3  39960  3dim1  39966  1cvratlt  39973  1cvrjat  39974  ps-1  39976  ps-2  39977  3atlem3  39984  3atlem5  39986  3atlem7  39988  llni  40007  llni2  40011  atcvrlln2  40018  llnexatN  40020  llncmp  40021  2llnmat  40023  2at0mat0  40024  lplni  40031  lplnnle2at  40040  2atnelpln  40043  lplnllnneN  40055  llncvrlpln2  40056  2lplnmN  40058  2llnmj  40059  lplncmp  40061  lplnexatN  40062  lplnexllnN  40063  2llnm3N  40068  lvoli  40074  lvoli3  40076  islvol2aN  40091  4atlem0a  40092  4atlem3  40095  4atlem3a  40096  4atlem4a  40098  4atlem4b  40099  4atlem4c  40100  4atlem4d  40101  4atlem10b  40104  4atlem11  40108  4atlem12  40111  lplncvrlvol2  40114  lvolcmp  40116  2lplnmj  40121  islinei  40239  pmapglbx  40268  linepmap  40274  lneq2at  40277  lnjatN  40279  lncvrat  40281  lncmp  40282  2llnma3r  40287  elpaddatriN  40302  elpaddat  40303  paddcom  40312  paddss1  40316  paddss2  40317  paddss12  40318  paddasslem6  40324  paddasslem7  40325  paddasslem8  40326  paddasslem9  40327  paddasslem15  40333  pmodlem2  40346  pmodl42N  40350  pmapjoin  40351  llnmod1i2  40359  2polcon4bN  40417  polcon2bN  40419  poml4N  40452  poml6N  40454  osumcllem1N  40455  osumcllem2N  40456  osumcllem11N  40465  osumclN  40466  pmapojoinN  40467  pexmidlem2N  40470  pexmidlem3N  40471  pexmidlem4N  40472  pexmidlem6N  40474  pexmidlem7N  40475  pl42lem2N  40479  pl42lem3N  40480  pl42lem4N  40481  pl42N  40482  lhpexle2lem  40508  lhpexle3lem  40510  lhpexle3  40511  lhpmcvr3  40524  lhp2at0nle  40534  lhprelat3N  40539  4atex  40575  4atex2  40576  lauteq  40594  lautco  40596  ltrncoidN  40627  ltrneq2  40647  ltrnnidn  40673  ltrnideq  40674  trlnid  40678  ltrnatlw  40682  trlnle  40685  trlval3  40686  trlval4  40687  cdlemc  40696  cdlemd5  40701  cdlemd9  40705  ltrneq3  40707  cdleme0moN  40724  cdleme20  40823  cdleme21j  40835  cdleme21  40836  cdleme27cl  40865  cdlemefrs29bpre0  40895  cdlemefs27cl  40912  cdlemefs32sn1aw  40913  cdleme43fsv1snlem  40919  cdleme32d  40943  cdleme32f  40945  cdleme32le  40946  cdleme35h2  40956  cdleme38n  40963  cdleme40m  40966  cdleme41snaw  40975  cdleme42ke  40984  cdleme17d3  40995  cdleme48fvg  40999  cdlemeg46fvcl  41005  cdlemeg46fgN  41033  cdleme48gfv1  41035  cdleme48fgv  41037  cdleme50trn3  41052  trlord  41068  ltrniotavalbN  41083  cdlemb3  41105  cdlemg6c  41119  cdlemg6  41122  cdlemg7N  41125  cdlemg8c  41128  cdlemg8  41130  cdlemg11a  41136  cdlemg11b  41141  cdlemg12e  41146  cdlemg15a  41154  cdlemg15  41155  cdlemg16  41156  cdlemg16z  41158  cdlemg16zz  41159  cdlemg17dN  41162  cdlemg18a  41177  cdlemg20  41184  cdlemg22  41186  cdlemg24  41187  cdlemg37  41188  cdlemg31d  41199  cdlemg29  41204  cdlemg33b  41206  cdlemg33  41210  cdlemg38  41214  cdlemg39  41215  cdlemg40  41216  trlco  41226  trlcone  41227  cdlemg42  41228  cdlemg44b  41231  ltrncom  41237  trljco  41239  tendococl  41271  tendoplcl  41280  tendoplcom  41281  cdlemj2  41321  cdlemj3  41322  tendoid0  41324  tendoconid  41328  tendotr  41329  cdlemk25-3  41403  cdlemk26b-3  41404  cdlemk34  41409  cdlemk36  41412  cdlemk38  41414  cdlemkid4  41433  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk19x  41442  cdlemk53  41456  cdlemk55  41460  cdlemk55u  41465  cdlemk39u  41467  cdlemk19u  41469  cdlemk56  41470  tendoex  41474  cdleml3N  41477  cdleml5N  41479  tendospcanN  41522  cdlemm10N  41617  cdlemn11pre  41709  dihord2pre  41724  dihvalcqpre  41734  dihopelvalcpre  41747  dihord6apre  41755  dihord5b  41758  dihord5apre  41761  dihord  41763  dihmeetlem1N  41789  dihglblem5apreN  41790  dihglblem3N  41794  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetbN  41802  dihmeetlem4preN  41805  dihmeetlem5  41807  dihmeetlem7N  41809  dihmeetlem10N  41815  dihmeetlem11N  41816  dihmeetlem12N  41817  dihmeetlem13N  41818  dihmeetlem15N  41820  dihmeetlem16N  41821  dihmeetlem17N  41822  dihmeetlem18N  41823  dihmeetlem19N  41824  dihmeetALTN  41826  dih1dimatlem0  41827  dihlspsnssN  41831  dihlspsnat  41832  mapdh8ad  42278  hdmap14lem14  42380  hgmapvvlem3  42424  aks6d1c6isolem1  42666  dvdsexpnn  42817  resubcan2  42872  mzprename  43205  eldioph2lem1  43216  lzunuz  43224  rencldnfi  43273  pellexlem2  43282  infmrgelbi  43330  pellfundglb  43337  pellfund14gap  43339  qirropth  43360  rmxycomplete  43369  congadd  43418  acongeq  43435  jm2.19  43445  jm2.23  43448  jm2.20nn  43449  jm2.27  43460  jm3.1  43472  aomclem6  43511  lnmepi  43537  lmhmfgsplit  43538  lmhmlnmsplit  43539  pwssplit4  43541  hbtlem2  43576  hbtlem5  43580  dgraa0p  43601  proot1hash  43647  iocunico  43663  oasubex  43738  oege1  43758  relexpxpmin  44168  brtrclfv2  44178  ntrclsiso  44518  ntrclskb  44520  ntrclsk3  44521  k0004lem3  44600  grur1cld  44683  ismnu  44712  grumnudlem  44736  suprnmpt  45628  wessf1ornlem  45639  projf1o  45650  snunioo1  45964  iccintsng  45975  lptre2pt  46090  limcleqr  46094  fnlimfvre  46124  limsupgtlem  46227  volioc  46422  iblspltprt  46423  stoweidlem19  46469  stoweidlem20  46470  stoweidlem22  46472  stoweidlem28  46478  stoweidlem34  46484  stoweidlem44  46494  stoweidlem60  46510  wallispilem3  46517  fourierdlem41  46598  fourierdlem42  46599  fourierdlem49  46605  fourierdlem51  46607  fourierdlem54  46610  fourierdlem74  46630  fourierdlem97  46653  caratheodorylem2  46977  ovnsubaddlem2  47021  hspmbllem2  47077  smflimmpt  47260  smflimsupmpt  47279  smfliminfmpt  47282  funfocofob  47548  fzopredsuc  47794  nnmul2b  47801  imasetpreimafvbijlemfv  47884  iccpartigtl  47905  lighneal  48096  oexpnegALTV  48175  oexpnegnz  48176  tgblthelfgott  48313  clnbgrgrim  48432  uhgrimgrlim  48485  gpgusgralem  48554  lidldomn1  48729  ofaddmndmap  48841  lincdifsn  48922  lincellss  48924  lincresunit3lem3  48972  islindeps2  48981  lindssnlvec  48984  fdivmptf  49039  refdivmptf  49040  rrx2linest  49240  itsclc0yqsollem1  49260  itsclc0b  49270  itsclquadb  49274  itscnhlinecirc02plem3  49282  diag1  49801  setc1onsubc  50099