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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl11  1248  simpl21  1251  simpl31  1254  simp1l1  1266  simp2l1  1272  simp3l1  1278  3anandirs  1472  rspc3ev  3628  2nreu  4441  predtrss  6323  frpomin  6341  f1prex  7281  cocan1  7288  weniso  7350  frrlem4  8273  frrlem10  8279  fprlem1  8284  smogt  8366  smocdmdom  8367  omeulem1  8581  nnmord  8631  nnmword  8632  naddasslem1  8692  naddasslem2  8693  difsnen  9052  enfixsn  9080  mapunen  9145  ac6sfi  9286  fipreima  9357  elfiun  9424  ordiso2  9509  wemaplem2  9541  en2eqpr  10001  indcardi  10035  fodomfi2  10054  iunfictbso  10108  infmap2  10212  cofsmo  10263  cfsmolem  10264  coftr  10267  fin23lem11  10311  fincssdom  10317  fin23lem26  10319  isf32lem9  10355  ac6num  10473  gchdomtri  10623  gchpwdom  10664  winainflem  10687  tskuni  10777  gruima  10796  gruf  10805  grudomon  10811  elnpi  10982  distrlem4pr  11020  prlem934  11027  addcan  11397  addcan2  11398  divmulass  11894  divmulasscom  11895  ltmul1a  12062  suprleub  12179  supmul1  12182  suprzcl  12641  uzsupss  12923  xleadd1a  13231  xlesubadd  13241  xmulasslem3  13264  xlemul2a  13267  xadddilem  13272  xadddi2  13275  ixxun  13339  icoshftf1o  13450  ioounsn  13453  snunioc  13456  lincmb01cmp  13471  iccf1o  13472  nn0p1elfzo  13674  fzofzim  13678  ltexp2a  14130  leexp2  14135  ltexp2r  14137  exple1  14140  expnlbnd2  14196  fun2dmnop0  14454  ccatass  14537  swrdswrdlem  14653  ccatopth  14665  repswpfx  14734  2cshw  14762  cshimadifsn  14779  cshimadifsn0  14780  cshco  14786  repsco  14790  s2f1o  14866  limsupgre  15424  addcn2  15537  mulcn2  15539  ntrivcvgmul  15847  binomrisefac  15985  dvdsmodexp  16204  dvdsadd2b  16248  dvdsexp2im  16269  dvdsmod  16271  oexpneg  16287  sadass  16411  gcdass  16488  rplpwr  16498  lcmfunsnlem1  16573  coprmdvds2  16590  rpmulgcd2  16592  qredeq  16593  rpdvds  16596  cncongr2  16604  rpexp  16658  prmdiveq  16718  hashgcdlem  16720  odzdvds  16727  modprmn0modprm0  16739  coprimeprodsq2  16741  pythagtriplem3  16750  pcdvdsb  16801  pcgcd1  16809  qexpz  16833  pockthg  16838  vdwnnlem1  16927  0ram  16952  ramz2  16956  lubss  18465  lubun  18467  clatleglb  18470  clatglbss  18471  mrelatglb  18512  isnsgrp  18613  issubmnd  18651  ress0g  18652  gsumccat  18721  frmdss2  18743  submefmnd  18775  mulgneg  18971  mulgdirlem  18984  submmulg  18997  subgmulg  19019  nmzsubg  19044  ghmmulg  19103  gsmsymgreqlem1  19297  pmtrfb  19332  psgnunilem4  19364  odmodnn0  19407  odnncl  19412  odmod  19413  odmulgid  19421  odmulgeq  19424  odf1o1  19439  odf1o2  19440  odngen  19444  gexdvdsi  19450  pgpfi1  19462  odcau  19471  subgslw  19483  fislw  19492  lsmssv  19510  lsmless1x  19511  lsmless2x  19512  lsmsubm  19520  lsmmod  19542  lsmmod2  19543  efgred  19615  cntzcmn  19707  ghmplusg  19713  odadd1  19715  odadd2  19716  odadd  19717  lsmcomx  19723  gsumconst  19801  ablsimpgprmd  19984  srg1zr  20037  ring1eq0  20109  mulgass2  20120  rhmdvdsr  20286  isabvd  20427  rmodislmodlem  20538  rmodislmod  20539  rmodislmodOLD  20540  lssintcl  20574  0lmhm  20650  lmhmvsca  20655  reslmhm2b  20664  pwssplit1  20669  pwssplit3  20671  lspfixed  20740  lspsnat  20757  lidldvgen  20892  xrsdsreclblem  20990  regsumsupp  21174  obselocv  21282  uvcresum  21347  frlmsslsp  21350  frlmup4  21355  lindff1  21374  f1lindf  21376  lsslindf  21384  islindf4  21392  lbslcic  21395  issubassa  21420  evlsval2  21649  psrplusgpropd  21757  coe1subfv  21787  coe1mul2  21790  mhmvlin  21898  mpomatmul  21947  mamutpos  21959  scmatscmide  22008  mavmulsolcl  22052  marrepcl  22065  mdetdiag  22100  mdetunilem1  22113  mdetunilem3  22115  mdetunilem7  22119  mdetunilem9  22121  mdetmul  22124  slesolinvbi  22182  m2pmfzmap  22248  pmatcollpwlem  22281  pmatcollpw  22282  mp2pm2mplem4  22310  chpdmatlem3  22341  chfacfisfcpmat  22356  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  chfacfpmmulgsum2  22366  cayhamlem1  22367  cpmidpmatlem2  22372  cpmadugsumlemB  22375  cpmadugsumlemC  22376  cpmadugsumlemF  22377  riinopn  22409  neiint  22607  topssnei  22627  restntr  22685  iscnp4  22766  cnconst2  22786  cnrest2  22789  cnprest2  22793  cnpdis  22796  cnt0  22849  cnt1  22853  cnhaus  22857  ordthauslem  22886  cncmp  22895  fiuncmp  22907  sscmp  22908  hauscmp  22910  cnconn  22925  unconn  22932  nlly2i  22979  llynlly  22980  nllyidm  22992  finlocfin  23023  ptrescn  23142  xkococnlem  23162  qtopss  23218  kqfvima  23233  r0cld  23241  ordthmeolem  23304  fbssint  23341  fmf  23448  fmss  23449  elfm  23450  rnelfmlem  23455  rnelfm  23456  fmco  23464  flimss2  23475  flimss1  23476  flimrest  23486  flftg  23499  cnpflf2  23503  cnpflf  23504  flfcnp  23507  supnfcls  23523  fclsss1  23525  fclsss2  23526  fcfnei  23538  fcfelbas  23539  cnpfcfi  23543  subgntr  23610  opnsubg  23611  cldsubg  23614  ghmcnp  23618  utop2nei  23754  neipcfilu  23800  bldisj  23903  blgt0  23904  bl2in  23905  blss2ps  23908  blss2  23909  blssps  23929  blss  23930  xmetresbl  23942  lpbl  24011  blcld  24013  stdbdbl  24025  metcnp3  24048  metcnp2  24050  txmetcnp  24055  blval2  24070  nmoix  24245  nmoeq0  24252  icoopnst  24454  iocopnst  24455  xrhmeo  24461  nmhmcn  24635  cphsqrtcl2  24702  cphsqrtcl3  24703  cfil3i  24785  caublcls  24825  bcthlem5  24844  cmetcusp1  24869  cssbn  24891  rrxcph  24908  pjth  24955  ovoliunlem2  25019  volun  25061  volsup2  25121  mbfimaopn2  25173  iblconst  25334  itgconst  25335  dvcnp2  25436  dvcn  25437  deg1mul3le  25633  deg1tmle  25634  dvdsq1p  25677  ig1peu  25688  ig1pdvds  25693  coeid3  25753  dgrmulc  25784  efcvx  25960  tanord  26046  logdivlti  26127  logccv  26170  recxpcl  26182  cxpeq  26262  ang180  26316  isosctrlem2  26321  cxp2lim  26478  amgm  26492  muval1  26634  dvdssqf  26639  mumullem2  26681  mumul  26682  bcmono  26777  lgsfcl2  26803  lgsdilem  26824  lgsdirprm  26831  lgsdir  26832  lgsdi  26834  lgsne0  26835  padicabv  27130  nosep1o  27181  nosep2o  27182  nosepssdm  27186  nolt02olem  27194  nosupres  27207  nosupbnd1lem1  27208  nosupbnd1lem4  27211  nosupbnd1lem5  27212  nosupbnd1lem6  27213  nosupbnd2  27216  noinfres  27222  noinfbnd1lem1  27223  noinfbnd1lem4  27226  noinfbnd1lem6  27228  noinfbnd2  27231  noetasuplem3  27235  noetalem1  27241  scutbdaybnd  27313  sltlpss  27398  coinitsslt  27403  addsass  27485  addsdi  27607  mulsass  27618  norecdiv  27635  brbtwn2  28160  colinearalglem1  28161  colinearalg  28165  axcgrtr  28170  axsegconlem8  28179  axsegconlem9  28180  axsegconlem10  28181  axcontlem8  28226  axcontlem10  28228  elntg2  28240  vtxdlfuhgr1v  28733  umgr2wlk  29200  erclwwlksym  29271  clwwlkfo  29300  clwwlkext2edg  29306  erclwwlknsym  29320  clwwlknon1  29347  numclwwlk2lem1  29626  numclwwlk5  29638  frgrregord13  29646  nvmul0or  29898  ipval2lem2  29952  lnomul  30008  shless  30607  shlej1  30608  pjspansn  30825  hoadddi  31051  kbmul  31203  homco2  31225  kbass2  31365  eliccelico  31983  elicoelioo  31984  iocinioc2  31985  iocinif  31987  swrdrn2  32113  xrge0adddir  32188  xrge0npcan  32190  archiabl  32339  ress1r  32378  pidlnz  32483  grplsm0l  32508  intlidl  32531  ssmxidl  32585  pstmfval  32871  fmcncfil  32906  zrhnm  32944  qqhnm  32965  measvunilem  33205  volfiniune  33223  dya2iocnrect  33275  sibfinima  33333  probun  33413  probinc  33415  cndprob01  33429  signstfvp  33577  bnj517  33891  bnj594  33918  pconnpi1  34223  cvmsss2  34260  mrsubcv  34496  msubvrs  34546  br6  34722  br4  34723  cgrcomim  34956  cgrtriv  34969  cgrextend  34975  segconeq  34977  btwntriv2  34979  btwnintr  34986  btwnexch3  34987  btwnouttr2  34989  trisegint  34995  cgrsub  35012  cgrxfr  35022  btwnxfr  35023  lineext  35043  btwnconn1lem13  35066  btwnconn1lem14  35067  btwnconn3  35070  segcon2  35072  brsegle  35075  brsegle2  35076  segletr  35081  segleantisym  35082  seglelin  35083  outsideofeu  35098  lineunray  35114  lineelsb2  35115  gg-dvcnp2  35169  ivthALT  35215  lindsenlbs  36478  areacirc  36576  cocanfo  36582  upixp  36592  ismtyima  36666  rrndstprj2  36694  zerdivemp1x  36810  lsatfixedN  37874  lssat  37881  eqlkr  37964  eqlkr2  37965  lkrlsp  37967  lshpkrlem4  37978  opposet  38046  cvrcon3b  38142  cvrcmp  38148  atlen0  38175  atnle  38182  atlatmstc  38184  cvlatexch3  38203  cvlsupr2  38208  hlsupr2  38253  hlrelat2  38269  cvrexchlem  38285  lnnat  38293  atcvrj2b  38298  atle  38302  atexchcvrN  38306  atbtwn  38312  athgt  38322  3dimlem3  38327  3dim1  38333  1cvratlt  38340  1cvrjat  38341  ps-1  38343  ps-2  38344  3atlem3  38351  3atlem5  38353  3atlem7  38355  llni  38374  llni2  38378  atcvrlln2  38385  llnexatN  38387  llncmp  38388  2llnmat  38390  2at0mat0  38391  lplni  38398  lplnnle2at  38407  2atnelpln  38410  lplnllnneN  38422  llncvrlpln2  38423  2lplnmN  38425  2llnmj  38426  lplncmp  38428  lplnexatN  38429  lplnexllnN  38430  2llnm3N  38435  lvoli  38441  lvoli3  38443  islvol2aN  38458  4atlem0a  38459  4atlem3  38462  4atlem3a  38463  4atlem4a  38465  4atlem4b  38466  4atlem4c  38467  4atlem4d  38468  4atlem10b  38471  4atlem11  38475  4atlem12  38478  lplncvrlvol2  38481  lvolcmp  38483  2lplnmj  38488  islinei  38606  pmapglbx  38635  linepmap  38641  lneq2at  38644  lnjatN  38646  lncvrat  38648  lncmp  38649  2llnma3r  38654  elpaddatriN  38669  elpaddat  38670  paddcom  38679  paddss1  38683  paddss2  38684  paddss12  38685  paddasslem6  38691  paddasslem7  38692  paddasslem8  38693  paddasslem9  38694  paddasslem15  38700  pmodlem2  38713  pmodl42N  38717  pmapjoin  38718  llnmod1i2  38726  2polcon4bN  38784  polcon2bN  38786  poml4N  38819  poml6N  38821  osumcllem1N  38822  osumcllem2N  38823  osumcllem11N  38832  osumclN  38833  pmapojoinN  38834  pexmidlem2N  38837  pexmidlem3N  38838  pexmidlem4N  38839  pexmidlem6N  38841  pexmidlem7N  38842  pl42lem2N  38846  pl42lem3N  38847  pl42lem4N  38848  pl42N  38849  lhpexle2lem  38875  lhpexle3lem  38877  lhpexle3  38878  lhpmcvr3  38891  lhp2at0nle  38901  lhprelat3N  38906  4atex  38942  4atex2  38943  lauteq  38961  lautco  38963  ltrncoidN  38994  ltrneq2  39014  ltrnnidn  39040  ltrnideq  39041  trlnid  39045  ltrnatlw  39049  trlnle  39052  trlval3  39053  trlval4  39054  cdlemc  39063  cdlemd5  39068  cdlemd9  39072  ltrneq3  39074  cdleme0moN  39091  cdleme20  39190  cdleme21j  39202  cdleme21  39203  cdleme27cl  39232  cdlemefrs29bpre0  39262  cdlemefs27cl  39279  cdlemefs32sn1aw  39280  cdleme43fsv1snlem  39286  cdleme32d  39310  cdleme32f  39312  cdleme32le  39313  cdleme35h2  39323  cdleme38n  39330  cdleme40m  39333  cdleme41snaw  39342  cdleme42ke  39351  cdleme17d3  39362  cdleme48fvg  39366  cdlemeg46fvcl  39372  cdlemeg46fgN  39400  cdleme48gfv1  39402  cdleme48fgv  39404  cdleme50trn3  39419  trlord  39435  ltrniotavalbN  39450  cdlemb3  39472  cdlemg6c  39486  cdlemg6  39489  cdlemg7N  39492  cdlemg8c  39495  cdlemg8  39497  cdlemg11a  39503  cdlemg11b  39508  cdlemg12e  39513  cdlemg15a  39521  cdlemg15  39522  cdlemg16  39523  cdlemg16z  39525  cdlemg16zz  39526  cdlemg17dN  39529  cdlemg18a  39544  cdlemg20  39551  cdlemg22  39553  cdlemg24  39554  cdlemg37  39555  cdlemg31d  39566  cdlemg29  39571  cdlemg33b  39573  cdlemg33  39577  cdlemg38  39581  cdlemg39  39582  cdlemg40  39583  trlco  39593  trlcone  39594  cdlemg42  39595  cdlemg44b  39598  ltrncom  39604  trljco  39606  tendococl  39638  tendoplcl  39647  tendoplcom  39648  cdlemj2  39688  cdlemj3  39689  tendoid0  39691  tendoconid  39695  tendotr  39696  cdlemk25-3  39770  cdlemk26b-3  39771  cdlemk34  39776  cdlemk36  39779  cdlemk38  39781  cdlemkid4  39800  cdlemk35s-id  39804  cdlemk39s-id  39806  cdlemk19x  39809  cdlemk53  39823  cdlemk55  39827  cdlemk55u  39832  cdlemk39u  39834  cdlemk19u  39836  cdlemk56  39837  tendoex  39841  cdleml3N  39844  cdleml5N  39846  tendospcanN  39889  cdlemm10N  39984  cdlemn11pre  40076  dihord2pre  40091  dihvalcqpre  40101  dihopelvalcpre  40114  dihord6apre  40122  dihord5b  40125  dihord5apre  40128  dihord  40130  dihmeetlem1N  40156  dihglblem5apreN  40157  dihglblem3N  40161  dihmeetlem2N  40165  dihglbcpreN  40166  dihmeetbN  40169  dihmeetlem4preN  40172  dihmeetlem5  40174  dihmeetlem7N  40176  dihmeetlem10N  40182  dihmeetlem11N  40183  dihmeetlem12N  40184  dihmeetlem13N  40185  dihmeetlem15N  40187  dihmeetlem16N  40188  dihmeetlem17N  40189  dihmeetlem18N  40190  dihmeetlem19N  40191  dihmeetALTN  40193  dih1dimatlem0  40194  dihlspsnssN  40198  dihlspsnat  40199  mapdh8ad  40645  hdmap14lem14  40747  hgmapvvlem3  40791  dvdsexpnn  41231  resubcan2  41262  mzprename  41477  eldioph2lem1  41488  lzunuz  41496  rencldnfi  41549  pellexlem2  41558  infmrgelbi  41606  pellfundglb  41613  pellfund14gap  41615  qirropth  41636  rmxycomplete  41646  congadd  41695  acongeq  41712  jm2.19  41722  jm2.23  41725  jm2.20nn  41726  jm2.27  41737  jm3.1  41749  aomclem6  41791  lnmepi  41817  lmhmfgsplit  41818  lmhmlnmsplit  41819  pwssplit4  41821  hbtlem2  41856  hbtlem5  41860  dgraa0p  41881  proot1hash  41932  iocunico  41950  oasubex  42026  oege1  42046  relexpxpmin  42458  brtrclfv2  42468  ntrclsiso  42808  ntrclskb  42810  ntrclsk3  42811  k0004lem3  42890  grur1cld  42981  ismnu  43010  grumnudlem  43034  suprnmpt  43860  wessf1ornlem  43872  projf1o  43886  snunioo1  44215  iccintsng  44226  lptre2pt  44346  limcleqr  44350  fnlimfvre  44380  limsupgtlem  44483  volioc  44678  iblspltprt  44679  stoweidlem19  44725  stoweidlem20  44726  stoweidlem22  44728  stoweidlem28  44734  stoweidlem34  44740  stoweidlem44  44750  stoweidlem60  44766  wallispilem3  44773  fourierdlem41  44854  fourierdlem42  44855  fourierdlem49  44861  fourierdlem51  44863  fourierdlem54  44866  fourierdlem74  44886  fourierdlem97  44909  caratheodorylem2  45233  ovnsubaddlem2  45277  hspmbllem2  45333  smflimmpt  45516  smflimsupmpt  45535  smfliminfmpt  45538  funfocofob  45776  fzopredsuc  46021  fzoopth  46025  imasetpreimafvbijlemfv  46060  iccpartigtl  46081  lighneal  46269  oexpnegALTV  46335  oexpnegnz  46336  tgblthelfgott  46473  rngisom1  46708  rnglidlrng  46748  2idlcpblrng  46756  lidldomn1  46813  ofaddmndmap  47009  lincdifsn  47095  lincellss  47097  lincresunit3lem3  47145  islindeps2  47154  lindssnlvec  47157  fdivmptf  47217  refdivmptf  47218  rrx2linest  47418  itsclc0yqsollem1  47438  itsclc0b  47448  itsclquadb  47452  itscnhlinecirc02plem3  47460