Theorem simpl1 1189

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

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

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 396  df-3an 1087

This theorem is referenced by:  simpl11  1246  simpl21  1249  simpl31  1252  simp1l1  1264  simp2l1  1270  simp3l1  1276  3anandirs  1470  rspc3ev  3566  2nreu  4372  predtrss  6214  frpomin  6228  f1prex  7136  cocan1  7143  weniso  7205  frrlem4  8076  frrlem10  8082  fprlem1  8087  smogt  8169  smorndom  8170  omeulem1  8375  nnmord  8425  nnmword  8426  difsnen  8794  enfixsn  8821  mapunen  8882  ac6sfi  8988  fipreima  9055  elfiun  9119  ordiso2  9204  wemaplem2  9236  en2eqpr  9694  indcardi  9728  fodomfi2  9747  iunfictbso  9801  infmap2  9905  cofsmo  9956  cfsmolem  9957  coftr  9960  fin23lem11  10004  fincssdom  10010  fin23lem26  10012  isf32lem9  10048  ac6num  10166  gchdomtri  10316  gchpwdom  10357  winainflem  10380  tskuni  10470  gruima  10489  gruf  10498  grudomon  10504  elnpi  10675  distrlem4pr  10713  prlem934  10720  addcan  11089  addcan2  11090  divmulass  11586  divmulasscom  11587  ltmul1a  11754  suprleub  11871  supmul1  11874  suprzcl  12330  uzsupss  12609  xleadd1a  12916  xlesubadd  12926  xmulasslem3  12949  xlemul2a  12952  xadddilem  12957  xadddi2  12960  ixxun  13024  icoshftf1o  13135  ioounsn  13138  snunioc  13141  lincmb01cmp  13156  iccf1o  13157  nn0p1elfzo  13358  fzofzim  13362  ltexp2a  13812  leexp2  13817  ltexp2r  13819  exple1  13822  expnlbnd2  13877  fun2dmnop0  14136  ccatass  14221  ccat2s1fvwOLD  14278  swrdswrdlem  14345  ccatopth  14357  repswpfx  14426  2cshw  14454  cshimadifsn  14470  cshimadifsn0  14471  cshco  14477  repsco  14481  s2f1o  14557  limsupgre  15118  addcn2  15231  mulcn2  15233  ntrivcvgmul  15542  binomrisefac  15680  dvdsmodexp  15899  dvdsadd2b  15943  dvdsexp2im  15964  dvdsmod  15966  oexpneg  15982  sadass  16106  gcdass  16183  rplpwr  16195  lcmfunsnlem1  16270  coprmdvds2  16287  rpmulgcd2  16289  qredeq  16290  rpdvds  16293  cncongr2  16301  rpexp  16355  prmdiveq  16415  hashgcdlem  16417  odzdvds  16424  modprmn0modprm0  16436  coprimeprodsq2  16438  pythagtriplem3  16447  pcdvdsb  16498  pcgcd1  16506  qexpz  16530  pockthg  16535  vdwnnlem1  16624  0ram  16649  ramz2  16653  lubss  18146  lubun  18148  clatleglb  18151  clatglbss  18152  mrelatglb  18193  isnsgrp  18294  issubmnd  18327  ress0g  18328  gsumccatOLD  18394  gsumccat  18395  frmdss2  18417  submefmnd  18449  mulgneg  18637  mulgdirlem  18649  submmulg  18662  subgmulg  18684  nmzsubg  18708  ghmmulg  18761  gsmsymgreqlem1  18953  pmtrfb  18988  psgnunilem4  19020  odmodnn0  19063  odnncl  19068  odmod  19069  odmulgid  19076  odmulgeq  19079  odf1o1  19092  odf1o2  19093  odngen  19097  gexdvdsi  19103  pgpfi1  19115  odcau  19124  subgslw  19136  fislw  19145  lsmssv  19163  lsmless1x  19164  lsmless2x  19165  lsmsubm  19173  lsmmod  19196  lsmmod2  19197  efgred  19269  cntzcmn  19356  ghmplusg  19362  odadd1  19364  odadd2  19365  odadd  19366  lsmcomx  19372  gsumconst  19450  ablsimpgprmd  19633  srg1zr  19680  ring1eq0  19744  mulgass2  19755  isabvd  19995  rmodislmodlem  20105  rmodislmod  20106  rmodislmodOLD  20107  lssintcl  20141  0lmhm  20217  lmhmvsca  20222  reslmhm2b  20231  pwssplit1  20236  pwssplit3  20238  lspfixed  20305  lspsnat  20322  lidldvgen  20439  xrsdsreclblem  20556  regsumsupp  20739  obselocv  20845  uvcresum  20910  frlmsslsp  20913  frlmup4  20918  lindff1  20937  f1lindf  20939  lsslindf  20947  islindf4  20955  lbslcic  20958  issubassa  20983  evlsval2  21207  psrplusgpropd  21317  coe1subfv  21347  coe1mul2  21350  mhmvlin  21456  mpomatmul  21503  mamutpos  21515  scmatscmide  21564  mavmulsolcl  21608  marrepcl  21621  mdetdiag  21656  mdetunilem1  21669  mdetunilem3  21671  mdetunilem7  21675  mdetunilem9  21677  mdetmul  21680  slesolinvbi  21738  m2pmfzmap  21804  pmatcollpwlem  21837  pmatcollpw  21838  mp2pm2mplem4  21866  chpdmatlem3  21897  chfacfisfcpmat  21912  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  chfacfpmmulgsum2  21922  cayhamlem1  21923  cpmidpmatlem2  21928  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  riinopn  21965  neiint  22163  topssnei  22183  restntr  22241  iscnp4  22322  cnconst2  22342  cnrest2  22345  cnprest2  22349  cnpdis  22352  cnt0  22405  cnt1  22409  cnhaus  22413  ordthauslem  22442  cncmp  22451  fiuncmp  22463  sscmp  22464  hauscmp  22466  cnconn  22481  unconn  22488  nlly2i  22535  llynlly  22536  nllyidm  22548  finlocfin  22579  ptrescn  22698  xkococnlem  22718  qtopss  22774  kqfvima  22789  r0cld  22797  ordthmeolem  22860  fbssint  22897  fmf  23004  fmss  23005  elfm  23006  rnelfmlem  23011  rnelfm  23012  fmco  23020  flimss2  23031  flimss1  23032  flimrest  23042  flftg  23055  cnpflf2  23059  cnpflf  23060  flfcnp  23063  supnfcls  23079  fclsss1  23081  fclsss2  23082  fcfnei  23094  fcfelbas  23095  cnpfcfi  23099  subgntr  23166  opnsubg  23167  cldsubg  23170  ghmcnp  23174  utop2nei  23310  neipcfilu  23356  bldisj  23459  blgt0  23460  bl2in  23461  blss2ps  23464  blss2  23465  blssps  23485  blss  23486  xmetresbl  23498  lpbl  23565  blcld  23567  stdbdbl  23579  metcnp3  23602  metcnp2  23604  txmetcnp  23609  blval2  23624  nmoix  23799  nmoeq0  23806  icoopnst  24008  iocopnst  24009  xrhmeo  24015  nmhmcn  24189  cphsqrtcl2  24255  cphsqrtcl3  24256  cfil3i  24338  caublcls  24378  bcthlem5  24397  cmetcusp1  24422  cssbn  24444  rrxcph  24461  pjth  24508  ovoliunlem2  24572  volun  24614  volsup2  24674  mbfimaopn2  24726  iblconst  24887  itgconst  24888  dvcnp2  24989  dvcn  24990  deg1mul3le  25186  deg1tmle  25187  dvdsq1p  25230  ig1peu  25241  ig1pdvds  25246  coeid3  25306  dgrmulc  25337  efcvx  25513  tanord  25599  logdivlti  25680  logccv  25723  recxpcl  25735  cxpeq  25815  ang180  25869  isosctrlem2  25874  cxp2lim  26031  amgm  26045  muval1  26187  dvdssqf  26192  mumullem2  26234  mumul  26235  bcmono  26330  lgsfcl2  26356  lgsdilem  26377  lgsdirprm  26384  lgsdir  26385  lgsdi  26387  lgsne0  26388  padicabv  26683  brbtwn2  27176  colinearalglem1  27177  colinearalg  27181  axcgrtr  27186  axsegconlem8  27195  axsegconlem9  27196  axsegconlem10  27197  axcontlem8  27242  axcontlem10  27244  elntg2  27256  vtxdlfuhgr1v  27749  umgr2wlk  28215  erclwwlksym  28286  clwwlkfo  28315  clwwlkext2edg  28321  erclwwlknsym  28335  clwwlknon1  28362  numclwwlk2lem1  28641  numclwwlk5  28653  frgrregord13  28661  nvmul0or  28913  ipval2lem2  28967  lnomul  29023  shless  29622  shlej1  29623  pjspansn  29840  hoadddi  30066  kbmul  30218  homco2  30240  kbass2  30380  eliccelico  31000  elicoelioo  31001  iocinioc2  31002  iocinif  31004  swrdrn2  31128  xrge0adddir  31203  xrge0npcan  31205  archiabl  31354  ress1r  31388  rhmdvdsr  31419  pidlnz  31473  grplsm0l  31493  intlidl  31504  ssmxidl  31544  pstmfval  31748  fmcncfil  31783  zrhnm  31819  qqhnm  31840  measvunilem  32080  volfiniune  32098  dya2iocnrect  32148  sibfinima  32206  probun  32286  probinc  32288  cndprob01  32302  signstfvp  32450  bnj517  32765  bnj594  32792  pconnpi1  33099  cvmsss2  33136  mrsubcv  33372  msubvrs  33422  br6  33630  br4  33631  nosep1o  33811  nosep2o  33812  nosepssdm  33816  nolt02olem  33824  nosupres  33837  nosupbnd1lem1  33838  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  nosupbnd2  33846  noinfres  33852  noinfbnd1lem1  33853  noinfbnd1lem4  33856  noinfbnd1lem6  33858  noinfbnd2  33861  noetasuplem3  33865  noetalem1  33871  scutbdaybnd  33936  sltlpss  34014  coinitsslt  34016  cgrcomim  34218  cgrtriv  34231  cgrextend  34237  segconeq  34239  btwntriv2  34241  btwnintr  34248  btwnexch3  34249  btwnouttr2  34251  trisegint  34257  cgrsub  34274  cgrxfr  34284  btwnxfr  34285  lineext  34305  btwnconn1lem13  34328  btwnconn1lem14  34329  btwnconn3  34332  segcon2  34334  brsegle  34337  brsegle2  34338  segletr  34343  segleantisym  34344  seglelin  34345  outsideofeu  34360  lineunray  34376  lineelsb2  34377  ivthALT  34451  lindsenlbs  35699  areacirc  35797  cocanfo  35803  upixp  35814  ismtyima  35888  rrndstprj2  35916  zerdivemp1x  36032  lsatfixedN  36950  lssat  36957  eqlkr  37040  eqlkr2  37041  lkrlsp  37043  lshpkrlem4  37054  opposet  37122  cvrcon3b  37218  cvrcmp  37224  atlen0  37251  atnle  37258  atlatmstc  37260  cvlatexch3  37279  cvlsupr2  37284  hlsupr2  37328  hlrelat2  37344  cvrexchlem  37360  lnnat  37368  atcvrj2b  37373  atle  37377  atexchcvrN  37381  atbtwn  37387  athgt  37397  3dimlem3  37402  3dim1  37408  1cvratlt  37415  1cvrjat  37416  ps-1  37418  ps-2  37419  3atlem3  37426  3atlem5  37428  3atlem7  37430  llni  37449  llni2  37453  atcvrlln2  37460  llnexatN  37462  llncmp  37463  2llnmat  37465  2at0mat0  37466  lplni  37473  lplnnle2at  37482  2atnelpln  37485  lplnllnneN  37497  llncvrlpln2  37498  2lplnmN  37500  2llnmj  37501  lplncmp  37503  lplnexatN  37504  lplnexllnN  37505  2llnm3N  37510  lvoli  37516  lvoli3  37518  islvol2aN  37533  4atlem0a  37534  4atlem3  37537  4atlem3a  37538  4atlem4a  37540  4atlem4b  37541  4atlem4c  37542  4atlem4d  37543  4atlem10b  37546  4atlem11  37550  4atlem12  37553  lplncvrlvol2  37556  lvolcmp  37558  2lplnmj  37563  islinei  37681  pmapglbx  37710  linepmap  37716  lneq2at  37719  lnjatN  37721  lncvrat  37723  lncmp  37724  2llnma3r  37729  elpaddatriN  37744  elpaddat  37745  paddcom  37754  paddss1  37758  paddss2  37759  paddss12  37760  paddasslem6  37766  paddasslem7  37767  paddasslem8  37768  paddasslem9  37769  paddasslem15  37775  pmodlem2  37788  pmodl42N  37792  pmapjoin  37793  llnmod1i2  37801  2polcon4bN  37859  polcon2bN  37861  poml4N  37894  poml6N  37896  osumcllem1N  37897  osumcllem2N  37898  osumcllem11N  37907  osumclN  37908  pmapojoinN  37909  pexmidlem2N  37912  pexmidlem3N  37913  pexmidlem4N  37914  pexmidlem6N  37916  pexmidlem7N  37917  pl42lem2N  37921  pl42lem3N  37922  pl42lem4N  37923  pl42N  37924  lhpexle2lem  37950  lhpexle3lem  37952  lhpexle3  37953  lhpmcvr3  37966  lhp2at0nle  37976  lhprelat3N  37981  4atex  38017  4atex2  38018  lauteq  38036  lautco  38038  ltrncoidN  38069  ltrneq2  38089  ltrnnidn  38115  ltrnideq  38116  trlnid  38120  ltrnatlw  38124  trlnle  38127  trlval3  38128  trlval4  38129  cdlemc  38138  cdlemd5  38143  cdlemd9  38147  ltrneq3  38149  cdleme0moN  38166  cdleme20  38265  cdleme21j  38277  cdleme21  38278  cdleme27cl  38307  cdlemefrs29bpre0  38337  cdlemefs27cl  38354  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme32d  38385  cdleme32f  38387  cdleme32le  38388  cdleme35h2  38398  cdleme38n  38405  cdleme40m  38408  cdleme41snaw  38417  cdleme42ke  38426  cdleme17d3  38437  cdleme48fvg  38441  cdlemeg46fvcl  38447  cdlemeg46fgN  38475  cdleme48gfv1  38477  cdleme48fgv  38479  cdleme50trn3  38494  trlord  38510  ltrniotavalbN  38525  cdlemb3  38547  cdlemg6c  38561  cdlemg6  38564  cdlemg7N  38567  cdlemg8c  38570  cdlemg8  38572  cdlemg11a  38578  cdlemg11b  38583  cdlemg12e  38588  cdlemg15a  38596  cdlemg15  38597  cdlemg16  38598  cdlemg16z  38600  cdlemg16zz  38601  cdlemg17dN  38604  cdlemg18a  38619  cdlemg20  38626  cdlemg22  38628  cdlemg24  38629  cdlemg37  38630  cdlemg31d  38641  cdlemg29  38646  cdlemg33b  38648  cdlemg33  38652  cdlemg38  38656  cdlemg39  38657  cdlemg40  38658  trlco  38668  trlcone  38669  cdlemg42  38670  cdlemg44b  38673  ltrncom  38679  trljco  38681  tendococl  38713  tendoplcl  38722  tendoplcom  38723  cdlemj2  38763  cdlemj3  38764  tendoid0  38766  tendoconid  38770  tendotr  38771  cdlemk25-3  38845  cdlemk26b-3  38846  cdlemk34  38851  cdlemk36  38854  cdlemk38  38856  cdlemkid4  38875  cdlemk35s-id  38879  cdlemk39s-id  38881  cdlemk19x  38884  cdlemk53  38898  cdlemk55  38902  cdlemk55u  38907  cdlemk39u  38909  cdlemk19u  38911  cdlemk56  38912  tendoex  38916  cdleml3N  38919  cdleml5N  38921  tendospcanN  38964  cdlemm10N  39059  cdlemn11pre  39151  dihord2pre  39166  dihvalcqpre  39176  dihopelvalcpre  39189  dihord6apre  39197  dihord5b  39200  dihord5apre  39203  dihord  39205  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem3N  39236  dihmeetlem2N  39240  dihglbcpreN  39241  dihmeetbN  39244  dihmeetlem4preN  39247  dihmeetlem5  39249  dihmeetlem7N  39251  dihmeetlem10N  39257  dihmeetlem11N  39258  dihmeetlem12N  39259  dihmeetlem13N  39260  dihmeetlem15N  39262  dihmeetlem16N  39263  dihmeetlem17N  39264  dihmeetlem18N  39265  dihmeetlem19N  39266  dihmeetALTN  39268  dih1dimatlem0  39269  dihlspsnssN  39273  dihlspsnat  39274  mapdh8ad  39720  hdmap14lem14  39822  hgmapvvlem3  39866  dvdsexpnn  40261  resubcan2  40292  mzprename  40487  eldioph2lem1  40498  lzunuz  40506  rencldnfi  40559  pellexlem2  40568  infmrgelbi  40616  pellfundglb  40623  pellfund14gap  40625  qirropth  40646  rmxycomplete  40655  congadd  40704  acongeq  40721  jm2.19  40731  jm2.23  40734  jm2.20nn  40735  jm2.27  40746  jm3.1  40758  aomclem6  40800  lnmepi  40826  lmhmfgsplit  40827  lmhmlnmsplit  40828  pwssplit4  40830  hbtlem2  40865  hbtlem5  40869  dgraa0p  40890  proot1hash  40941  iocunico  40958  relexpxpmin  41214  brtrclfv2  41224  ntrclsiso  41566  ntrclskb  41568  ntrclsk3  41569  k0004lem3  41648  grur1cld  41739  ismnu  41768  grumnudlem  41792  suprnmpt  42599  wessf1ornlem  42611  projf1o  42625  snunioo1  42940  iccintsng  42951  lptre2pt  43071  limcleqr  43075  fnlimfvre  43105  limsupgtlem  43208  volioc  43403  iblspltprt  43404  stoweidlem19  43450  stoweidlem20  43451  stoweidlem22  43453  stoweidlem28  43459  stoweidlem34  43465  stoweidlem44  43475  stoweidlem60  43491  wallispilem3  43498  fourierdlem41  43579  fourierdlem42  43580  fourierdlem49  43586  fourierdlem51  43588  fourierdlem54  43591  fourierdlem74  43611  fourierdlem97  43634  caratheodorylem2  43955  ovnsubaddlem2  43999  hspmbllem2  44055  smflimmpt  44230  smflimsupmpt  44249  smfliminfmpt  44252  funfocofob  44457  fzopredsuc  44703  fzoopth  44707  imasetpreimafvbijlemfv  44742  iccpartigtl  44763  lighneal  44951  oexpnegALTV  45017  oexpnegnz  45018  tgblthelfgott  45155  lidldomn1  45367  ofaddmndmap  45567  lincdifsn  45653  lincellss  45655  lincresunit3lem3  45703  islindeps2  45712  lindssnlvec  45715  fdivmptf  45775  refdivmptf  45776  rrx2linest  45976  itsclc0yqsollem1  45996  itsclc0b  46006  itsclquadb  46010  itscnhlinecirc02plem3  46018