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

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

This theorem is referenced by:  simpl11  1247  simpl21  1250  simpl31  1253  simp1l1  1265  simp2l1  1271  simp3l1  1277  3anandirs  1471  rspc3ev  3638  2nreu  4449  predtrss  6344  frpomin  6362  f1prex  7303  cocan1  7310  weniso  7373  frrlem4  8312  frrlem10  8318  fprlem1  8323  smogt  8405  smocdmdom  8406  omeulem1  8618  nnmord  8668  nnmword  8669  naddasslem1  8730  naddasslem2  8731  difsnen  9091  enfixsn  9119  mapunen  9184  ac6sfi  9317  fipreima  9395  elfiun  9467  ordiso2  9552  wemaplem2  9584  en2eqpr  10044  indcardi  10078  fodomfi2  10097  iunfictbso  10151  infmap2  10254  cofsmo  10306  cfsmolem  10307  coftr  10310  fin23lem11  10354  fincssdom  10360  fin23lem26  10362  isf32lem9  10398  ac6num  10516  gchdomtri  10666  gchpwdom  10707  winainflem  10730  tskuni  10820  gruima  10839  gruf  10848  grudomon  10854  elnpi  11025  distrlem4pr  11063  prlem934  11070  addcan  11442  addcan2  11443  divmulass  11942  divmulasscom  11943  ltmul1a  12113  suprleub  12231  supmul1  12234  suprzcl  12695  uzsupss  12979  xleadd1a  13291  xlesubadd  13301  xmulasslem3  13324  xlemul2a  13327  xadddilem  13332  xadddi2  13335  ixxun  13399  icoshftf1o  13510  ioounsn  13513  snunioc  13516  lincmb01cmp  13531  iccf1o  13532  nn0p1elfzo  13738  fzofzim  13745  fzoopth  13797  ltexp2a  14202  leexp2  14207  ltexp2r  14209  exple1  14212  expnlbnd2  14269  fun2dmnop0  14539  ccatass  14622  swrdswrdlem  14738  ccatopth  14750  repswpfx  14819  2cshw  14847  cshimadifsn  14864  cshimadifsn0  14865  cshco  14871  repsco  14875  s2f1o  14951  limsupgre  15513  addcn2  15626  mulcn2  15628  ntrivcvgmul  15934  binomrisefac  16074  dvdsmodexp  16294  dvdsadd2b  16339  dvdsexp2im  16360  dvdsmod  16362  oexpneg  16378  sadass  16504  gcdass  16580  rplpwr  16591  lcmfunsnlem1  16670  coprmdvds2  16687  rpmulgcd2  16689  qredeq  16690  rpdvds  16693  cncongr2  16701  rpexp  16755  prmdiveq  16819  hashgcdlem  16821  odzdvds  16828  modprmn0modprm0  16840  coprimeprodsq2  16842  pythagtriplem3  16851  pcdvdsb  16902  pcgcd1  16910  qexpz  16934  pockthg  16939  vdwnnlem1  17028  0ram  17053  ramz2  17057  lubss  18570  lubun  18572  clatleglb  18575  clatglbss  18576  mrelatglb  18617  isnsgrp  18748  issubmnd  18786  ress0g  18787  mhmvlin  18826  gsumccat  18866  frmdss2  18888  submefmnd  18920  mulgneg  19122  mulgdirlem  19135  submmulg  19148  subgmulg  19170  nmzsubg  19195  ghmmulg  19258  gsmsymgreqlem1  19462  pmtrfb  19497  psgnunilem4  19529  odmodnn0  19572  odnncl  19577  odmod  19578  odmulgid  19586  odmulgeq  19589  odf1o1  19604  odf1o2  19605  odngen  19609  gexdvdsi  19615  pgpfi1  19627  odcau  19636  subgslw  19648  fislw  19657  lsmssv  19675  lsmless1x  19676  lsmless2x  19677  lsmsubm  19685  lsmmod  19707  lsmmod2  19708  efgred  19780  cntzcmn  19872  ghmplusg  19878  odadd1  19880  odadd2  19881  odadd  19882  lsmcomx  19888  gsumconst  19966  ablsimpgprmd  20149  srg1zr  20232  ring1eq0  20311  mulgass2  20322  rngisom1  20482  rhmdvdsr  20524  isabvd  20829  rmodislmodlem  20943  rmodislmod  20944  rmodislmodOLD  20945  lssintcl  20979  0lmhm  21056  lmhmvsca  21061  reslmhm2b  21070  pwssplit1  21075  pwssplit3  21077  lspfixed  21147  lspsnat  21164  rnglidlrng  21274  2idlcpblrng  21298  lidldvgen  21361  xrsdsreclblem  21447  regsumsupp  21657  obselocv  21765  uvcresum  21830  frlmsslsp  21833  frlmup4  21838  lindff1  21857  f1lindf  21859  lsslindf  21867  islindf4  21875  lbslcic  21878  issubassa  21904  evlsval2  22128  psrplusgpropd  22252  coe1subfv  22284  coe1mul2  22287  mpomatmul  22467  mamutpos  22479  scmatscmide  22528  mavmulsolcl  22572  marrepcl  22585  mdetdiag  22620  mdetunilem1  22633  mdetunilem3  22635  mdetunilem7  22639  mdetunilem9  22641  mdetmul  22644  slesolinvbi  22702  m2pmfzmap  22768  pmatcollpwlem  22801  pmatcollpw  22802  mp2pm2mplem4  22830  chpdmatlem3  22861  chfacfisfcpmat  22876  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  chfacfpmmulgsum2  22886  cayhamlem1  22887  cpmidpmatlem2  22892  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  riinopn  22929  neiint  23127  topssnei  23147  restntr  23205  iscnp4  23286  cnconst2  23306  cnrest2  23309  cnprest2  23313  cnpdis  23316  cnt0  23369  cnt1  23373  cnhaus  23377  ordthauslem  23406  cncmp  23415  fiuncmp  23427  sscmp  23428  hauscmp  23430  cnconn  23445  unconn  23452  nlly2i  23499  llynlly  23500  nllyidm  23512  finlocfin  23543  ptrescn  23662  xkococnlem  23682  qtopss  23738  kqfvima  23753  r0cld  23761  ordthmeolem  23824  fbssint  23861  fmf  23968  fmss  23969  elfm  23970  rnelfmlem  23975  rnelfm  23976  fmco  23984  flimss2  23995  flimss1  23996  flimrest  24006  flftg  24019  cnpflf2  24023  cnpflf  24024  flfcnp  24027  supnfcls  24043  fclsss1  24045  fclsss2  24046  fcfnei  24058  fcfelbas  24059  cnpfcfi  24063  subgntr  24130  opnsubg  24131  cldsubg  24134  ghmcnp  24138  utop2nei  24274  neipcfilu  24320  bldisj  24423  blgt0  24424  bl2in  24425  blss2ps  24428  blss2  24429  blssps  24449  blss  24450  xmetresbl  24462  lpbl  24531  blcld  24533  stdbdbl  24545  metcnp3  24568  metcnp2  24570  txmetcnp  24575  blval2  24590  nmoix  24765  nmoeq0  24772  icoopnst  24982  iocopnst  24983  xrhmeo  24990  nmhmcn  25166  cphsqrtcl2  25233  cphsqrtcl3  25234  cfil3i  25316  caublcls  25356  bcthlem5  25375  cmetcusp1  25400  cssbn  25422  rrxcph  25439  pjth  25486  ovoliunlem2  25551  volun  25593  volsup2  25653  mbfimaopn2  25705  iblconst  25867  itgconst  25868  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  deg1mul3le  26170  deg1tmle  26171  dvdsq1p  26216  ig1peu  26228  ig1pdvds  26233  coeid3  26293  dgrmulc  26325  efcvx  26507  tanord  26594  logdivlti  26676  logccv  26719  recxpcl  26731  cxpeq  26814  ang180  26871  isosctrlem2  26876  cxp2lim  27034  amgm  27048  muval1  27190  dvdssqf  27195  mumullem2  27237  mumul  27238  bcmono  27335  lgsfcl2  27361  lgsdilem  27382  lgsdirprm  27389  lgsdir  27390  lgsdi  27392  lgsne0  27393  padicabv  27688  nosep1o  27740  nosep2o  27741  nosepssdm  27745  nolt02olem  27753  nosupres  27766  nosupbnd1lem1  27767  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  nosupbnd2  27775  noinfres  27781  noinfbnd1lem1  27782  noinfbnd1lem4  27785  noinfbnd1lem6  27787  noinfbnd2  27790  noetasuplem3  27794  noetalem1  27800  scutbdaybnd  27874  sltlpss  27959  slelss  27960  coinitsslt  27967  addsass  28052  addsdi  28195  mulsass  28206  norecdiv  28230  brbtwn2  28934  colinearalglem1  28935  colinearalg  28939  axcgrtr  28944  axsegconlem8  28953  axsegconlem9  28954  axsegconlem10  28955  axcontlem8  29000  axcontlem10  29002  elntg2  29014  vtxdlfuhgr1v  29511  umgr2wlk  29978  erclwwlksym  30049  clwwlkfo  30078  clwwlkext2edg  30084  erclwwlknsym  30098  clwwlknon1  30125  numclwwlk2lem1  30404  numclwwlk5  30416  frgrregord13  30424  nvmul0or  30678  ipval2lem2  30732  lnomul  30788  shless  31387  shlej1  31388  pjspansn  31605  hoadddi  31831  kbmul  31983  homco2  32005  kbass2  32145  eliccelico  32785  elicoelioo  32786  iocinioc2  32787  iocinif  32789  swrdrn2  32923  xrge0adddir  33005  xrge0npcan  33007  archiabl  33187  ress1r  33223  pidlnz  33383  grplsm0l  33410  intlidl  33427  ssmxidl  33481  pstmfval  33856  fmcncfil  33891  zrhnm  33929  qqhnm  33952  measvunilem  34192  volfiniune  34210  dya2iocnrect  34262  sibfinima  34320  probun  34400  probinc  34402  cndprob01  34416  signstfvp  34564  bnj517  34877  bnj594  34904  pconnpi1  35221  cvmsss2  35258  mrsubcv  35494  msubvrs  35544  br6  35736  br4  35737  cgrcomim  35970  cgrtriv  35983  cgrextend  35989  segconeq  35991  btwntriv2  35993  btwnintr  36000  btwnexch3  36001  btwnouttr2  36003  trisegint  36009  cgrsub  36026  cgrxfr  36036  btwnxfr  36037  lineext  36057  btwnconn1lem13  36080  btwnconn1lem14  36081  btwnconn3  36084  segcon2  36086  brsegle  36089  brsegle2  36090  segletr  36095  segleantisym  36096  seglelin  36097  outsideofeu  36112  lineunray  36128  lineelsb2  36129  ivthALT  36317  weiunpo  36447  weiunso  36448  weiunfr  36449  weiunse  36450  lindsenlbs  37601  areacirc  37699  cocanfo  37705  upixp  37715  ismtyima  37789  rrndstprj2  37817  zerdivemp1x  37933  lsatfixedN  38990  lssat  38997  eqlkr  39080  eqlkr2  39081  lkrlsp  39083  lshpkrlem4  39094  opposet  39162  cvrcon3b  39258  cvrcmp  39264  atlen0  39291  atnle  39298  atlatmstc  39300  cvlatexch3  39319  cvlsupr2  39324  hlsupr2  39369  hlrelat2  39385  cvrexchlem  39401  lnnat  39409  atcvrj2b  39414  atle  39418  atexchcvrN  39422  atbtwn  39428  athgt  39438  3dimlem3  39443  3dim1  39449  1cvratlt  39456  1cvrjat  39457  ps-1  39459  ps-2  39460  3atlem3  39467  3atlem5  39469  3atlem7  39471  llni  39490  llni2  39494  atcvrlln2  39501  llnexatN  39503  llncmp  39504  2llnmat  39506  2at0mat0  39507  lplni  39514  lplnnle2at  39523  2atnelpln  39526  lplnllnneN  39538  llncvrlpln2  39539  2lplnmN  39541  2llnmj  39542  lplncmp  39544  lplnexatN  39545  lplnexllnN  39546  2llnm3N  39551  lvoli  39557  lvoli3  39559  islvol2aN  39574  4atlem0a  39575  4atlem3  39578  4atlem3a  39579  4atlem4a  39581  4atlem4b  39582  4atlem4c  39583  4atlem4d  39584  4atlem10b  39587  4atlem11  39591  4atlem12  39594  lplncvrlvol2  39597  lvolcmp  39599  2lplnmj  39604  islinei  39722  pmapglbx  39751  linepmap  39757  lneq2at  39760  lnjatN  39762  lncvrat  39764  lncmp  39765  2llnma3r  39770  elpaddatriN  39785  elpaddat  39786  paddcom  39795  paddss1  39799  paddss2  39800  paddss12  39801  paddasslem6  39807  paddasslem7  39808  paddasslem8  39809  paddasslem9  39810  paddasslem15  39816  pmodlem2  39829  pmodl42N  39833  pmapjoin  39834  llnmod1i2  39842  2polcon4bN  39900  polcon2bN  39902  poml4N  39935  poml6N  39937  osumcllem1N  39938  osumcllem2N  39939  osumcllem11N  39948  osumclN  39949  pmapojoinN  39950  pexmidlem2N  39953  pexmidlem3N  39954  pexmidlem4N  39955  pexmidlem6N  39957  pexmidlem7N  39958  pl42lem2N  39962  pl42lem3N  39963  pl42lem4N  39964  pl42N  39965  lhpexle2lem  39991  lhpexle3lem  39993  lhpexle3  39994  lhpmcvr3  40007  lhp2at0nle  40017  lhprelat3N  40022  4atex  40058  4atex2  40059  lauteq  40077  lautco  40079  ltrncoidN  40110  ltrneq2  40130  ltrnnidn  40156  ltrnideq  40157  trlnid  40161  ltrnatlw  40165  trlnle  40168  trlval3  40169  trlval4  40170  cdlemc  40179  cdlemd5  40184  cdlemd9  40188  ltrneq3  40190  cdleme0moN  40207  cdleme20  40306  cdleme21j  40318  cdleme21  40319  cdleme27cl  40348  cdlemefrs29bpre0  40378  cdlemefs27cl  40395  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme32d  40426  cdleme32f  40428  cdleme32le  40429  cdleme35h2  40439  cdleme38n  40446  cdleme40m  40449  cdleme41snaw  40458  cdleme42ke  40467  cdleme17d3  40478  cdleme48fvg  40482  cdlemeg46fvcl  40488  cdlemeg46fgN  40516  cdleme48gfv1  40518  cdleme48fgv  40520  cdleme50trn3  40535  trlord  40551  ltrniotavalbN  40566  cdlemb3  40588  cdlemg6c  40602  cdlemg6  40605  cdlemg7N  40608  cdlemg8c  40611  cdlemg8  40613  cdlemg11a  40619  cdlemg11b  40624  cdlemg12e  40629  cdlemg15a  40637  cdlemg15  40638  cdlemg16  40639  cdlemg16z  40641  cdlemg16zz  40642  cdlemg17dN  40645  cdlemg18a  40660  cdlemg20  40667  cdlemg22  40669  cdlemg24  40670  cdlemg37  40671  cdlemg31d  40682  cdlemg29  40687  cdlemg33b  40689  cdlemg33  40693  cdlemg38  40697  cdlemg39  40698  cdlemg40  40699  trlco  40709  trlcone  40710  cdlemg42  40711  cdlemg44b  40714  ltrncom  40720  trljco  40722  tendococl  40754  tendoplcl  40763  tendoplcom  40764  cdlemj2  40804  cdlemj3  40805  tendoid0  40807  tendoconid  40811  tendotr  40812  cdlemk25-3  40886  cdlemk26b-3  40887  cdlemk34  40892  cdlemk36  40895  cdlemk38  40897  cdlemkid4  40916  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk19x  40925  cdlemk53  40939  cdlemk55  40943  cdlemk55u  40948  cdlemk39u  40950  cdlemk19u  40952  cdlemk56  40953  tendoex  40957  cdleml3N  40960  cdleml5N  40962  tendospcanN  41005  cdlemm10N  41100  cdlemn11pre  41192  dihord2pre  41207  dihvalcqpre  41217  dihopelvalcpre  41230  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dihord  41246  dihmeetlem1N  41272  dihglblem5apreN  41273  dihglblem3N  41277  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetbN  41285  dihmeetlem4preN  41288  dihmeetlem5  41290  dihmeetlem7N  41292  dihmeetlem10N  41298  dihmeetlem11N  41299  dihmeetlem12N  41300  dihmeetlem13N  41301  dihmeetlem15N  41303  dihmeetlem16N  41304  dihmeetlem17N  41305  dihmeetlem18N  41306  dihmeetlem19N  41307  dihmeetALTN  41309  dih1dimatlem0  41310  dihlspsnssN  41314  dihlspsnat  41315  mapdh8ad  41761  hdmap14lem14  41863  hgmapvvlem3  41907  aks6d1c6isolem1  42155  dvdsexpnn  42346  resubcan2  42394  mzprename  42736  eldioph2lem1  42747  lzunuz  42755  rencldnfi  42808  pellexlem2  42817  infmrgelbi  42865  pellfundglb  42872  pellfund14gap  42874  qirropth  42895  rmxycomplete  42905  congadd  42954  acongeq  42971  jm2.19  42981  jm2.23  42984  jm2.20nn  42985  jm2.27  42996  jm3.1  43008  aomclem6  43047  lnmepi  43073  lmhmfgsplit  43074  lmhmlnmsplit  43075  pwssplit4  43077  hbtlem2  43112  hbtlem5  43116  dgraa0p  43137  proot1hash  43183  iocunico  43199  oasubex  43275  oege1  43295  relexpxpmin  43706  brtrclfv2  43716  ntrclsiso  44056  ntrclskb  44058  ntrclsk3  44059  k0004lem3  44138  grur1cld  44227  ismnu  44256  grumnudlem  44280  suprnmpt  45116  wessf1ornlem  45127  projf1o  45139  snunioo1  45464  iccintsng  45475  lptre2pt  45595  limcleqr  45599  fnlimfvre  45629  limsupgtlem  45732  volioc  45927  iblspltprt  45928  stoweidlem19  45974  stoweidlem20  45975  stoweidlem22  45977  stoweidlem28  45983  stoweidlem34  45989  stoweidlem44  45999  stoweidlem60  46015  wallispilem3  46022  fourierdlem41  46103  fourierdlem42  46104  fourierdlem49  46110  fourierdlem51  46112  fourierdlem54  46115  fourierdlem74  46135  fourierdlem97  46158  caratheodorylem2  46482  ovnsubaddlem2  46526  hspmbllem2  46582  smflimmpt  46765  smflimsupmpt  46784  smfliminfmpt  46787  funfocofob  47027  fzopredsuc  47272  imasetpreimafvbijlemfv  47326  iccpartigtl  47347  lighneal  47535  oexpnegALTV  47601  oexpnegnz  47602  tgblthelfgott  47739  clnbgrgrim  47839  uhgrimgrlim  47889  gpgusgralem  47945  lidldomn1  48074  ofaddmndmap  48187  lincdifsn  48269  lincellss  48271  lincresunit3lem3  48319  islindeps2  48328  lindssnlvec  48331  fdivmptf  48390  refdivmptf  48391  rrx2linest  48591  itsclc0yqsollem1  48611  itsclc0b  48621  itsclquadb  48625  itscnhlinecirc02plem3  48633