Theorem simpl1 1204

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  simpl11  1261  simpl21  1264  simpl31  1267  simp1l1  1279  simp2l1  1285  simp3l1  1291  3anandirs  1492  rspc3ev  3598  2nreu  4397  predtrss  6305  frpomin  6323  f1prex  7264  cocan1  7271  weniso  7334  frrlem4  8265  frrlem10  8271  fprlem1  8276  smogt  8333  smocdmdom  8334  omeulem1  8546  nnmord  8597  nnmword  8598  naddasslem1  8660  naddasslem2  8661  difsnen  9027  enfixsn  9054  mapunen  9114  ac6sfi  9224  fipreima  9298  elfiun  9373  ordiso2  9460  wemaplem2  9492  en2eqpr  9960  indcardi  9994  fodomfi2  10013  iunfictbso  10067  infmap2  10170  cofsmo  10223  cfsmolem  10224  coftr  10227  fin23lem11  10271  fincssdom  10277  fin23lem26  10279  isf32lem9  10315  ac6num  10433  gchdomtri  10584  gchpwdom  10625  winainflem  10648  tskuni  10738  gruima  10757  gruf  10766  grudomon  10772  elnpi  10943  distrlem4pr  10981  prlem934  10988  addcan  11364  addcan2  11365  divmulass  11865  divmulasscom  11866  ltmul1a  12037  suprleub  12155  supmul1  12158  suprzcl  12650  uzsupss  12938  xleadd1a  13253  xlesubadd  13263  xmulasslem3  13286  xlemul2a  13289  xadddilem  13294  xadddi2  13297  ixxun  13362  icoshftf1o  13475  ioounsn  13478  snunioc  13481  lincmb01cmp  13496  iccf1o  13497  nn0p1elfzo  13705  fzofzim  13712  fzoopth  13765  ltexp2a  14176  leexp2  14181  ltexp2r  14183  exple1  14187  expnlbnd2  14244  fun2dmnop0  14514  ccatass  14599  swrdswrdlem  14714  ccatopth  14726  repswpfx  14795  2cshw  14823  cshimadifsn  14839  cshimadifsn0  14840  cshco  14846  repsco  14850  s2f1o  14926  limsupgre  15491  addcn2  15604  mulcn2  15606  ntrivcvgmul  15915  binomrisefac  16055  dvdsmodexp  16277  dvdsadd2b  16323  dvdsexp2im  16344  dvdsmod  16346  oexpneg  16362  sadass  16488  gcdass  16564  rplpwr  16575  lcmfunsnlem1  16654  coprmdvds2  16671  rpmulgcd2  16673  qredeq  16674  rpdvds  16677  cncongr2  16685  rpexp  16740  prmdiveq  16804  hashgcdlem  16806  odzdvds  16814  modprmn0modprm0  16826  coprimeprodsq2  16828  pythagtriplem3  16837  pcdvdsb  16888  pcgcd1  16896  qexpz  16920  pockthg  16925  vdwnnlem1  17014  0ram  17039  ramz2  17043  lubss  18528  lubun  18530  clatleglb  18533  clatglbss  18534  mrelatglb  18575  isnsgrp  18740  issubmnd  18778  ress0g  18779  mhmvlin  18818  gsumccat  18858  frmdss2  18880  submefmnd  18912  mulgneg  19117  mulgdirlem  19130  submmulg  19143  subgmulg  19165  nmzsubg  19189  ghmmulg  19251  gsmsymgreqlem1  19453  pmtrfb  19488  psgnunilem4  19520  odmodnn0  19563  odnncl  19568  odmod  19569  odmulgid  19577  odmulgeq  19580  odf1o1  19595  odf1o2  19596  odngen  19600  gexdvdsi  19606  pgpfi1  19618  odcau  19627  subgslw  19639  fislw  19648  lsmssv  19666  lsmless1x  19667  lsmless2x  19668  lsmsubm  19676  lsmmod  19698  lsmmod2  19699  efgred  19771  cntzcmn  19863  ghmplusg  19869  odadd1  19871  odadd2  19872  odadd  19873  lsmcomx  19879  gsumconst  19957  ablsimpgprmd  20140  srg1zr  20244  ring1eq0  20327  mulgass2  20338  rngisom1  20494  rhmdvdsr  20537  isabvd  20841  rmodislmodlem  20976  rmodislmod  20977  lssintcl  21011  0lmhm  21087  lmhmvsca  21092  reslmhm2b  21101  pwssplit1  21106  pwssplit3  21108  lspfixed  21178  lspsnat  21195  rnglidlrng  21297  2idlcpblrng  21321  lidldvgen  21384  xrsdsreclblem  21445  regsumsupp  21654  obselocv  21760  uvcresum  21825  frlmsslsp  21828  frlmup4  21833  lindff1  21852  f1lindf  21854  lsslindf  21862  islindf4  21870  lbslcic  21873  issubassa  21899  evlsval2  22120  psrplusgpropd  22277  coe1subfv  22309  coe1mul2  22312  mpomatmul  22486  mamutpos  22498  scmatscmide  22547  mavmulsolcl  22591  marrepcl  22604  mdetdiag  22639  mdetunilem1  22652  mdetunilem3  22654  mdetunilem7  22658  mdetunilem9  22660  mdetmul  22663  slesolinvbi  22721  m2pmfzmap  22787  pmatcollpwlem  22820  pmatcollpw  22821  mp2pm2mplem4  22849  chpdmatlem3  22880  chfacfisfcpmat  22895  chfacfscmulgsum  22900  chfacfpmmulgsum  22904  chfacfpmmulgsum2  22905  cayhamlem1  22906  cpmidpmatlem2  22911  cpmadugsumlemB  22914  cpmadugsumlemC  22915  cpmadugsumlemF  22916  riinopn  22948  neiint  23144  topssnei  23164  restntr  23222  iscnp4  23303  cnconst2  23323  cnrest2  23326  cnprest2  23330  cnpdis  23333  cnt0  23386  cnt1  23390  cnhaus  23394  ordthauslem  23423  cncmp  23432  fiuncmp  23444  sscmp  23445  hauscmp  23447  cnconn  23462  unconn  23469  nlly2i  23516  llynlly  23517  nllyidm  23529  finlocfin  23560  ptrescn  23679  xkococnlem  23699  qtopss  23755  kqfvima  23770  r0cld  23778  ordthmeolem  23841  fbssint  23878  fmf  23985  fmss  23986  elfm  23987  rnelfmlem  23992  rnelfm  23993  fmco  24001  flimss2  24012  flimss1  24013  flimrest  24023  flftg  24036  cnpflf2  24040  cnpflf  24041  flfcnp  24044  supnfcls  24060  fclsss1  24062  fclsss2  24063  fcfnei  24075  fcfelbas  24076  cnpfcfi  24080  subgntr  24147  opnsubg  24148  cldsubg  24151  ghmcnp  24155  utop2nei  24290  neipcfilu  24335  bldisj  24438  blgt0  24439  bl2in  24440  blss2ps  24443  blss2  24444  blssps  24464  blss  24465  xmetresbl  24477  lpbl  24543  blcld  24545  stdbdbl  24557  metcnp3  24580  metcnp2  24582  txmetcnp  24587  blval2  24602  nmoix  24769  nmoeq0  24776  icoopnst  24981  iocopnst  24982  xrhmeo  24988  nmhmcn  25162  cphsqrtcl2  25228  cphsqrtcl3  25229  cfil3i  25311  caublcls  25351  bcthlem5  25370  cmetcusp1  25395  cssbn  25417  rrxcph  25434  pjth  25481  ovoliunlem2  25545  volun  25587  volsup2  25647  mbfimaopn2  25699  iblconst  25860  itgconst  25861  dvcnp2  25962  dvcn  25963  deg1mul3le  26157  deg1tmle  26158  dvdsq1p  26203  ig1peu  26215  ig1pdvds  26220  coeid3  26280  dgrmulc  26311  efcvx  26489  tanord  26580  logdivlti  26662  logccv  26705  recxpcl  26717  cxpeq  26799  ang180  26856  isosctrlem2  26861  cxp2lim  27018  amgm  27032  muval1  27174  dvdssqf  27179  mumullem2  27221  mumul  27222  bcmono  27318  lgsfcl2  27344  lgsdilem  27365  lgsdirprm  27372  lgsdir  27373  lgsdi  27375  lgsne0  27376  padicabv  27671  nosep1o  27722  nosep2o  27723  nosepssdm  27727  nolt02olem  27735  nosupres  27748  nosupbnd1lem1  27749  nosupbnd1lem4  27752  nosupbnd1lem5  27753  nosupbnd1lem6  27754  nosupbnd2  27757  noinfres  27763  noinfbnd1lem1  27764  noinfbnd1lem4  27767  noinfbnd1lem6  27769  noinfbnd2  27772  noetasuplem3  27776  noetalem1  27782  cutbdaybnd  27865  ltslpss  27978  leslss  27979  coinitslts  27989  addsass  28075  addsdi  28225  mulsass  28236  norecdiv  28260  bdayfinbndlem1  28537  z12bdaylem  28554  brbtwn2  29052  colinearalglem1  29053  colinearalg  29057  axcgrtr  29062  axsegconlem8  29071  axsegconlem9  29072  axsegconlem10  29073  axcontlem8  29118  axcontlem10  29120  elntg2  29132  vtxdlfuhgr1v  29626  umgr2wlk  30095  erclwwlksym  30169  clwwlkfo  30198  clwwlkext2edg  30204  erclwwlknsym  30218  clwwlknon1  30245  numclwwlk2lem1  30524  numclwwlk5  30536  frgrregord13  30544  nvmul0or  30799  ipval2lem2  30853  lnomul  30909  shless  31508  shlej1  31509  pjspansn  31726  hoadddi  31952  kbmul  32104  homco2  32126  kbass2  32266  eliccelico  32929  elicoelioo  32930  iocinioc2  32931  iocinif  32933  swrdrn2  33093  xrge0adddir  33157  xrge0npcan  33159  archiabl  33339  ress1r  33374  pidlnz  33523  grplsm0l  33550  intlidl  33567  ssmxidl  33623  pstmfval  34154  fmcncfil  34189  zrhnm  34225  qqhnm  34248  measvunilem  34470  volfiniune  34488  dya2iocnrect  34539  sibfinima  34597  probun  34677  probinc  34679  cndprob01  34693  signstfvp  34829  bnj517  35144  bnj594  35171  fissorduni  35349  pconnpi1  35551  cvmsss2  35588  mrsubcv  35824  msubvrs  35874  br6  36071  br4  36072  cgrcomim  36303  cgrtriv  36316  cgrextend  36322  segconeq  36324  btwntriv2  36326  btwnintr  36333  btwnexch3  36334  btwnouttr2  36336  trisegint  36342  cgrsub  36359  cgrxfr  36369  btwnxfr  36370  lineext  36390  btwnconn1lem13  36413  btwnconn1lem14  36414  btwnconn3  36417  segcon2  36419  brsegle  36422  brsegle2  36423  segletr  36428  segleantisym  36429  seglelin  36430  outsideofeu  36445  lineunray  36461  lineelsb2  36462  ivthALT  36659  weiunpo  36789  weiunso  36790  weiunfr  36791  weiunse  36792  lindsenlbs  38078  areacirc  38176  cocanfo  38182  upixp  38192  ismtyima  38266  rrndstprj2  38294  zerdivemp1x  38410  lsatfixedN  39597  lssat  39604  eqlkr  39687  eqlkr2  39688  lkrlsp  39690  lshpkrlem4  39701  opposet  39769  cvrcon3b  39865  cvrcmp  39871  atlen0  39898  atnle  39905  atlatmstc  39907  cvlatexch3  39926  cvlsupr2  39931  hlsupr2  39975  hlrelat2  39991  cvrexchlem  40007  lnnat  40015  atcvrj2b  40020  atle  40024  atexchcvrN  40028  atbtwn  40034  athgt  40044  3dimlem3  40049  3dim1  40055  1cvratlt  40062  1cvrjat  40063  ps-1  40065  ps-2  40066  3atlem3  40073  3atlem5  40075  3atlem7  40077  llni  40096  llni2  40100  atcvrlln2  40107  llnexatN  40109  llncmp  40110  2llnmat  40112  2at0mat0  40113  lplni  40120  lplnnle2at  40129  2atnelpln  40132  lplnllnneN  40144  llncvrlpln2  40145  2lplnmN  40147  2llnmj  40148  lplncmp  40150  lplnexatN  40151  lplnexllnN  40152  2llnm3N  40157  lvoli  40163  lvoli3  40165  islvol2aN  40180  4atlem0a  40181  4atlem3  40184  4atlem3a  40185  4atlem4a  40187  4atlem4b  40188  4atlem4c  40189  4atlem4d  40190  4atlem10b  40193  4atlem11  40197  4atlem12  40200  lplncvrlvol2  40203  lvolcmp  40205  2lplnmj  40210  islinei  40328  pmapglbx  40357  linepmap  40363  lneq2at  40366  lnjatN  40368  lncvrat  40370  lncmp  40371  2llnma3r  40376  elpaddatriN  40391  elpaddat  40392  paddcom  40401  paddss1  40405  paddss2  40406  paddss12  40407  paddasslem6  40413  paddasslem7  40414  paddasslem8  40415  paddasslem9  40416  paddasslem15  40422  pmodlem2  40435  pmodl42N  40439  pmapjoin  40440  llnmod1i2  40448  2polcon4bN  40506  polcon2bN  40508  poml4N  40541  poml6N  40543  osumcllem1N  40544  osumcllem2N  40545  osumcllem11N  40554  osumclN  40555  pmapojoinN  40556  pexmidlem2N  40559  pexmidlem3N  40560  pexmidlem4N  40561  pexmidlem6N  40563  pexmidlem7N  40564  pl42lem2N  40568  pl42lem3N  40569  pl42lem4N  40570  pl42N  40571  lhpexle2lem  40597  lhpexle3lem  40599  lhpexle3  40600  lhpmcvr3  40613  lhp2at0nle  40623  lhprelat3N  40628  4atex  40664  4atex2  40665  lauteq  40683  lautco  40685  ltrncoidN  40716  ltrneq2  40736  ltrnnidn  40762  ltrnideq  40763  trlnid  40767  ltrnatlw  40771  trlnle  40774  trlval3  40775  trlval4  40776  cdlemc  40785  cdlemd5  40790  cdlemd9  40794  ltrneq3  40796  cdleme0moN  40813  cdleme20  40912  cdleme21j  40924  cdleme21  40925  cdleme27cl  40954  cdlemefrs29bpre0  40984  cdlemefs27cl  41001  cdlemefs32sn1aw  41002  cdleme43fsv1snlem  41008  cdleme32d  41032  cdleme32f  41034  cdleme32le  41035  cdleme35h2  41045  cdleme38n  41052  cdleme40m  41055  cdleme41snaw  41064  cdleme42ke  41073  cdleme17d3  41084  cdleme48fvg  41088  cdlemeg46fvcl  41094  cdlemeg46fgN  41122  cdleme48gfv1  41124  cdleme48fgv  41126  cdleme50trn3  41141  trlord  41157  ltrniotavalbN  41172  cdlemb3  41194  cdlemg6c  41208  cdlemg6  41211  cdlemg7N  41214  cdlemg8c  41217  cdlemg8  41219  cdlemg11a  41225  cdlemg11b  41230  cdlemg12e  41235  cdlemg15a  41243  cdlemg15  41244  cdlemg16  41245  cdlemg16z  41247  cdlemg16zz  41248  cdlemg17dN  41251  cdlemg18a  41266  cdlemg20  41273  cdlemg22  41275  cdlemg24  41276  cdlemg37  41277  cdlemg31d  41288  cdlemg29  41293  cdlemg33b  41295  cdlemg33  41299  cdlemg38  41303  cdlemg39  41304  cdlemg40  41305  trlco  41315  trlcone  41316  cdlemg42  41317  cdlemg44b  41320  ltrncom  41326  trljco  41328  tendococl  41360  tendoplcl  41369  tendoplcom  41370  cdlemj2  41410  cdlemj3  41411  tendoid0  41413  tendoconid  41417  tendotr  41418  cdlemk25-3  41492  cdlemk26b-3  41493  cdlemk34  41498  cdlemk36  41501  cdlemk38  41503  cdlemkid4  41522  cdlemk35s-id  41526  cdlemk39s-id  41528  cdlemk19x  41531  cdlemk53  41545  cdlemk55  41549  cdlemk55u  41554  cdlemk39u  41556  cdlemk19u  41558  cdlemk56  41559  tendoex  41563  cdleml3N  41566  cdleml5N  41568  tendospcanN  41611  cdlemm10N  41706  cdlemn11pre  41798  dihord2pre  41813  dihvalcqpre  41823  dihopelvalcpre  41836  dihord6apre  41844  dihord5b  41847  dihord5apre  41850  dihord  41852  dihmeetlem1N  41878  dihglblem5apreN  41879  dihglblem3N  41883  dihmeetlem2N  41887  dihglbcpreN  41888  dihmeetbN  41891  dihmeetlem4preN  41894  dihmeetlem5  41896  dihmeetlem7N  41898  dihmeetlem10N  41904  dihmeetlem11N  41905  dihmeetlem12N  41906  dihmeetlem13N  41907  dihmeetlem15N  41909  dihmeetlem16N  41910  dihmeetlem17N  41911  dihmeetlem18N  41912  dihmeetlem19N  41913  dihmeetALTN  41915  dih1dimatlem0  41916  dihlspsnssN  41920  dihlspsnat  41921  mapdh8ad  42367  hdmap14lem14  42469  hgmapvvlem3  42513  aks6d1c6isolem1  42755  dvdsexpnn  42906  resubcan2  42961  mzprename  43294  eldioph2lem1  43305  lzunuz  43313  rencldnfi  43362  pellexlem2  43371  infmrgelbi  43419  pellfundglb  43426  pellfund14gap  43428  qirropth  43449  rmxycomplete  43458  congadd  43507  acongeq  43524  jm2.19  43534  jm2.23  43537  jm2.20nn  43538  jm2.27  43549  jm3.1  43561  aomclem6  43600  lnmepi  43626  lmhmfgsplit  43627  lmhmlnmsplit  43628  pwssplit4  43630  hbtlem2  43665  hbtlem5  43669  dgraa0p  43690  proot1hash  43736  iocunico  43752  oasubex  43827  oege1  43847  relexpxpmin  44257  brtrclfv2  44267  ntrclsiso  44607  ntrclskb  44609  ntrclsk3  44610  k0004lem3  44689  grur1cld  44772  ismnu  44801  grumnudlem  44825  suprnmpt  45716  wessf1ornlem  45727  projf1o  45738  snunioo1  46052  iccintsng  46063  lptre2pt  46178  limcleqr  46182  fnlimfvre  46212  limsupgtlem  46315  volioc  46510  iblspltprt  46511  stoweidlem19  46557  stoweidlem20  46558  stoweidlem22  46560  stoweidlem28  46566  stoweidlem34  46572  stoweidlem44  46582  stoweidlem60  46598  wallispilem3  46605  fourierdlem41  46686  fourierdlem42  46687  fourierdlem49  46693  fourierdlem51  46695  fourierdlem54  46698  fourierdlem74  46718  fourierdlem97  46741  caratheodorylem2  47065  ovnsubaddlem2  47109  hspmbllem2  47165  smflimmpt  47348  smflimsupmpt  47367  smfliminfmpt  47370  funfocofob  47636  fzopredsuc  47882  nnmul2b  47889  imasetpreimafvbijlemfv  47972  iccpartigtl  47993  lighneal  48184  oexpnegALTV  48263  oexpnegnz  48264  tgblthelfgott  48401  clnbgrgrim  48520  uhgrimgrlim  48573  gpgusgralem  48642  lidldomn1  48817  ofaddmndmap  48929  lincdifsn  49010  lincellss  49012  lincresunit3lem3  49060  islindeps2  49069  lindssnlvec  49072  fdivmptf  49127  refdivmptf  49128  rrx2linest  49328  itsclc0yqsollem1  49348  itsclc0b  49358  itsclquadb  49362  itscnhlinecirc02plem3  49370  diag1  49889  setc1onsubc  50187