Theorem simpl1 1193

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

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

This theorem is referenced by:  simpl11  1250  simpl21  1253  simpl31  1256  simp1l1  1268  simp2l1  1274  simp3l1  1280  3anandirs  1475  rspc3ev  3582  2nreu  4385  predtrss  6280  frpomin  6298  f1prex  7232  cocan1  7239  weniso  7302  frrlem4  8232  frrlem10  8238  fprlem1  8243  smogt  8300  smocdmdom  8301  omeulem1  8510  nnmord  8561  nnmword  8562  naddasslem1  8623  naddasslem2  8624  difsnen  8990  enfixsn  9017  mapunen  9077  ac6sfi  9187  fipreima  9261  elfiun  9336  ordiso2  9423  wemaplem2  9455  en2eqpr  9920  indcardi  9954  fodomfi2  9973  iunfictbso  10027  infmap2  10130  cofsmo  10182  cfsmolem  10183  coftr  10186  fin23lem11  10230  fincssdom  10236  fin23lem26  10238  isf32lem9  10274  ac6num  10392  gchdomtri  10543  gchpwdom  10584  winainflem  10607  tskuni  10697  gruima  10716  gruf  10725  grudomon  10731  elnpi  10902  distrlem4pr  10940  prlem934  10947  addcan  11321  addcan2  11322  divmulass  11823  divmulasscom  11824  ltmul1a  11995  suprleub  12113  supmul1  12116  suprzcl  12600  uzsupss  12881  xleadd1a  13196  xlesubadd  13206  xmulasslem3  13229  xlemul2a  13232  xadddilem  13237  xadddi2  13240  ixxun  13305  icoshftf1o  13418  ioounsn  13421  snunioc  13424  lincmb01cmp  13439  iccf1o  13440  nn0p1elfzo  13648  fzofzim  13655  fzoopth  13708  ltexp2a  14119  leexp2  14124  ltexp2r  14126  exple1  14130  expnlbnd2  14187  fun2dmnop0  14457  ccatass  14542  swrdswrdlem  14657  ccatopth  14669  repswpfx  14738  2cshw  14766  cshimadifsn  14782  cshimadifsn0  14783  cshco  14789  repsco  14793  s2f1o  14869  limsupgre  15434  addcn2  15547  mulcn2  15549  ntrivcvgmul  15858  binomrisefac  15998  dvdsmodexp  16220  dvdsadd2b  16266  dvdsexp2im  16287  dvdsmod  16289  oexpneg  16305  sadass  16431  gcdass  16507  rplpwr  16518  lcmfunsnlem1  16597  coprmdvds2  16614  rpmulgcd2  16616  qredeq  16617  rpdvds  16620  cncongr2  16628  rpexp  16683  prmdiveq  16747  hashgcdlem  16749  odzdvds  16757  modprmn0modprm0  16769  coprimeprodsq2  16771  pythagtriplem3  16780  pcdvdsb  16831  pcgcd1  16839  qexpz  16863  pockthg  16868  vdwnnlem1  16957  0ram  16982  ramz2  16986  lubss  18470  lubun  18472  clatleglb  18475  clatglbss  18476  mrelatglb  18517  isnsgrp  18682  issubmnd  18720  ress0g  18721  mhmvlin  18760  gsumccat  18800  frmdss2  18822  submefmnd  18854  mulgneg  19059  mulgdirlem  19072  submmulg  19085  subgmulg  19107  nmzsubg  19131  ghmmulg  19194  gsmsymgreqlem1  19396  pmtrfb  19431  psgnunilem4  19463  odmodnn0  19506  odnncl  19511  odmod  19512  odmulgid  19520  odmulgeq  19523  odf1o1  19538  odf1o2  19539  odngen  19543  gexdvdsi  19549  pgpfi1  19561  odcau  19570  subgslw  19582  fislw  19591  lsmssv  19609  lsmless1x  19610  lsmless2x  19611  lsmsubm  19619  lsmmod  19641  lsmmod2  19642  efgred  19714  cntzcmn  19806  ghmplusg  19812  odadd1  19814  odadd2  19815  odadd  19816  lsmcomx  19822  gsumconst  19900  ablsimpgprmd  20083  srg1zr  20187  ring1eq0  20270  mulgass2  20281  rngisom1  20437  rhmdvdsr  20476  isabvd  20780  rmodislmodlem  20915  rmodislmod  20916  lssintcl  20950  0lmhm  21027  lmhmvsca  21032  reslmhm2b  21041  pwssplit1  21046  pwssplit3  21048  lspfixed  21118  lspsnat  21135  rnglidlrng  21237  2idlcpblrng  21261  lidldvgen  21324  xrsdsreclblem  21402  regsumsupp  21612  obselocv  21718  uvcresum  21783  frlmsslsp  21786  frlmup4  21791  lindff1  21810  f1lindf  21812  lsslindf  21820  islindf4  21828  lbslcic  21831  issubassa  21857  evlsval2  22075  psrplusgpropd  22209  coe1subfv  22241  coe1mul2  22244  mpomatmul  22421  mamutpos  22433  scmatscmide  22482  mavmulsolcl  22526  marrepcl  22539  mdetdiag  22574  mdetunilem1  22587  mdetunilem3  22589  mdetunilem7  22593  mdetunilem9  22595  mdetmul  22598  slesolinvbi  22656  m2pmfzmap  22722  pmatcollpwlem  22755  pmatcollpw  22756  mp2pm2mplem4  22784  chpdmatlem3  22815  chfacfisfcpmat  22830  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  chfacfpmmulgsum2  22840  cayhamlem1  22841  cpmidpmatlem2  22846  cpmadugsumlemB  22849  cpmadugsumlemC  22850  cpmadugsumlemF  22851  riinopn  22883  neiint  23079  topssnei  23099  restntr  23157  iscnp4  23238  cnconst2  23258  cnrest2  23261  cnprest2  23265  cnpdis  23268  cnt0  23321  cnt1  23325  cnhaus  23329  ordthauslem  23358  cncmp  23367  fiuncmp  23379  sscmp  23380  hauscmp  23382  cnconn  23397  unconn  23404  nlly2i  23451  llynlly  23452  nllyidm  23464  finlocfin  23495  ptrescn  23614  xkococnlem  23634  qtopss  23690  kqfvima  23705  r0cld  23713  ordthmeolem  23776  fbssint  23813  fmf  23920  fmss  23921  elfm  23922  rnelfmlem  23927  rnelfm  23928  fmco  23936  flimss2  23947  flimss1  23948  flimrest  23958  flftg  23971  cnpflf2  23975  cnpflf  23976  flfcnp  23979  supnfcls  23995  fclsss1  23997  fclsss2  23998  fcfnei  24010  fcfelbas  24011  cnpfcfi  24015  subgntr  24082  opnsubg  24083  cldsubg  24086  ghmcnp  24090  utop2nei  24225  neipcfilu  24270  bldisj  24373  blgt0  24374  bl2in  24375  blss2ps  24378  blss2  24379  blssps  24399  blss  24400  xmetresbl  24412  lpbl  24478  blcld  24480  stdbdbl  24492  metcnp3  24515  metcnp2  24517  txmetcnp  24522  blval2  24537  nmoix  24704  nmoeq0  24711  icoopnst  24916  iocopnst  24917  xrhmeo  24923  nmhmcn  25097  cphsqrtcl2  25163  cphsqrtcl3  25164  cfil3i  25246  caublcls  25286  bcthlem5  25305  cmetcusp1  25330  cssbn  25352  rrxcph  25369  pjth  25416  ovoliunlem2  25480  volun  25522  volsup2  25582  mbfimaopn2  25634  iblconst  25795  itgconst  25796  dvcnp2  25897  dvcn  25898  deg1mul3le  26092  deg1tmle  26093  dvdsq1p  26138  ig1peu  26150  ig1pdvds  26155  coeid3  26215  dgrmulc  26246  efcvx  26427  tanord  26515  logdivlti  26597  logccv  26640  recxpcl  26652  cxpeq  26734  ang180  26791  isosctrlem2  26796  cxp2lim  26954  amgm  26968  muval1  27110  dvdssqf  27115  mumullem2  27157  mumul  27158  bcmono  27254  lgsfcl2  27280  lgsdilem  27301  lgsdirprm  27308  lgsdir  27309  lgsdi  27311  lgsne0  27312  padicabv  27607  nosep1o  27659  nosep2o  27660  nosepssdm  27664  nolt02olem  27672  nosupres  27685  nosupbnd1lem1  27686  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd1lem6  27691  nosupbnd2  27694  noinfres  27700  noinfbnd1lem1  27701  noinfbnd1lem4  27704  noinfbnd1lem6  27706  noinfbnd2  27709  noetasuplem3  27713  noetalem1  27719  cutbdaybnd  27801  ltslpss  27914  leslss  27915  coinitslts  27925  addsass  28011  addsdi  28161  mulsass  28172  norecdiv  28196  bdayfinbndlem1  28473  z12bdaylem  28490  brbtwn2  28988  colinearalglem1  28989  colinearalg  28993  axcgrtr  28998  axsegconlem8  29007  axsegconlem9  29008  axsegconlem10  29009  axcontlem8  29054  axcontlem10  29056  elntg2  29068  vtxdlfuhgr1v  29563  umgr2wlk  30032  erclwwlksym  30106  clwwlkfo  30135  clwwlkext2edg  30141  erclwwlknsym  30155  clwwlknon1  30182  numclwwlk2lem1  30461  numclwwlk5  30473  frgrregord13  30481  nvmul0or  30736  ipval2lem2  30790  lnomul  30846  shless  31445  shlej1  31446  pjspansn  31663  hoadddi  31889  kbmul  32041  homco2  32063  kbass2  32203  eliccelico  32865  elicoelioo  32866  iocinioc2  32867  iocinif  32869  swrdrn2  33029  xrge0adddir  33093  xrge0npcan  33095  archiabl  33274  ress1r  33309  pidlnz  33451  grplsm0l  33478  intlidl  33495  ssmxidl  33549  pstmfval  34056  fmcncfil  34091  zrhnm  34127  qqhnm  34150  measvunilem  34372  volfiniune  34390  dya2iocnrect  34441  sibfinima  34499  probun  34579  probinc  34581  cndprob01  34595  signstfvp  34731  bnj517  35043  bnj594  35070  fissorduni  35249  pconnpi1  35435  cvmsss2  35472  mrsubcv  35708  msubvrs  35758  br6  35955  br4  35956  cgrcomim  36187  cgrtriv  36200  cgrextend  36206  segconeq  36208  btwntriv2  36210  btwnintr  36217  btwnexch3  36218  btwnouttr2  36220  trisegint  36226  cgrsub  36243  cgrxfr  36253  btwnxfr  36254  lineext  36274  btwnconn1lem13  36297  btwnconn1lem14  36298  btwnconn3  36301  segcon2  36303  brsegle  36306  brsegle2  36307  segletr  36312  segleantisym  36313  seglelin  36314  outsideofeu  36329  lineunray  36345  lineelsb2  36346  ivthALT  36533  weiunpo  36663  weiunso  36664  weiunfr  36665  weiunse  36666  lindsenlbs  37950  areacirc  38048  cocanfo  38054  upixp  38064  ismtyima  38138  rrndstprj2  38166  zerdivemp1x  38282  lsatfixedN  39469  lssat  39476  eqlkr  39559  eqlkr2  39560  lkrlsp  39562  lshpkrlem4  39573  opposet  39641  cvrcon3b  39737  cvrcmp  39743  atlen0  39770  atnle  39777  atlatmstc  39779  cvlatexch3  39798  cvlsupr2  39803  hlsupr2  39847  hlrelat2  39863  cvrexchlem  39879  lnnat  39887  atcvrj2b  39892  atle  39896  atexchcvrN  39900  atbtwn  39906  athgt  39916  3dimlem3  39921  3dim1  39927  1cvratlt  39934  1cvrjat  39935  ps-1  39937  ps-2  39938  3atlem3  39945  3atlem5  39947  3atlem7  39949  llni  39968  llni2  39972  atcvrlln2  39979  llnexatN  39981  llncmp  39982  2llnmat  39984  2at0mat0  39985  lplni  39992  lplnnle2at  40001  2atnelpln  40004  lplnllnneN  40016  llncvrlpln2  40017  2lplnmN  40019  2llnmj  40020  lplncmp  40022  lplnexatN  40023  lplnexllnN  40024  2llnm3N  40029  lvoli  40035  lvoli3  40037  islvol2aN  40052  4atlem0a  40053  4atlem3  40056  4atlem3a  40057  4atlem4a  40059  4atlem4b  40060  4atlem4c  40061  4atlem4d  40062  4atlem10b  40065  4atlem11  40069  4atlem12  40072  lplncvrlvol2  40075  lvolcmp  40077  2lplnmj  40082  islinei  40200  pmapglbx  40229  linepmap  40235  lneq2at  40238  lnjatN  40240  lncvrat  40242  lncmp  40243  2llnma3r  40248  elpaddatriN  40263  elpaddat  40264  paddcom  40273  paddss1  40277  paddss2  40278  paddss12  40279  paddasslem6  40285  paddasslem7  40286  paddasslem8  40287  paddasslem9  40288  paddasslem15  40294  pmodlem2  40307  pmodl42N  40311  pmapjoin  40312  llnmod1i2  40320  2polcon4bN  40378  polcon2bN  40380  poml4N  40413  poml6N  40415  osumcllem1N  40416  osumcllem2N  40417  osumcllem11N  40426  osumclN  40427  pmapojoinN  40428  pexmidlem2N  40431  pexmidlem3N  40432  pexmidlem4N  40433  pexmidlem6N  40435  pexmidlem7N  40436  pl42lem2N  40440  pl42lem3N  40441  pl42lem4N  40442  pl42N  40443  lhpexle2lem  40469  lhpexle3lem  40471  lhpexle3  40472  lhpmcvr3  40485  lhp2at0nle  40495  lhprelat3N  40500  4atex  40536  4atex2  40537  lauteq  40555  lautco  40557  ltrncoidN  40588  ltrneq2  40608  ltrnnidn  40634  ltrnideq  40635  trlnid  40639  ltrnatlw  40643  trlnle  40646  trlval3  40647  trlval4  40648  cdlemc  40657  cdlemd5  40662  cdlemd9  40666  ltrneq3  40668  cdleme0moN  40685  cdleme20  40784  cdleme21j  40796  cdleme21  40797  cdleme27cl  40826  cdlemefrs29bpre0  40856  cdlemefs27cl  40873  cdlemefs32sn1aw  40874  cdleme43fsv1snlem  40880  cdleme32d  40904  cdleme32f  40906  cdleme32le  40907  cdleme35h2  40917  cdleme38n  40924  cdleme40m  40927  cdleme41snaw  40936  cdleme42ke  40945  cdleme17d3  40956  cdleme48fvg  40960  cdlemeg46fvcl  40966  cdlemeg46fgN  40994  cdleme48gfv1  40996  cdleme48fgv  40998  cdleme50trn3  41013  trlord  41029  ltrniotavalbN  41044  cdlemb3  41066  cdlemg6c  41080  cdlemg6  41083  cdlemg7N  41086  cdlemg8c  41089  cdlemg8  41091  cdlemg11a  41097  cdlemg11b  41102  cdlemg12e  41107  cdlemg15a  41115  cdlemg15  41116  cdlemg16  41117  cdlemg16z  41119  cdlemg16zz  41120  cdlemg17dN  41123  cdlemg18a  41138  cdlemg20  41145  cdlemg22  41147  cdlemg24  41148  cdlemg37  41149  cdlemg31d  41160  cdlemg29  41165  cdlemg33b  41167  cdlemg33  41171  cdlemg38  41175  cdlemg39  41176  cdlemg40  41177  trlco  41187  trlcone  41188  cdlemg42  41189  cdlemg44b  41192  ltrncom  41198  trljco  41200  tendococl  41232  tendoplcl  41241  tendoplcom  41242  cdlemj2  41282  cdlemj3  41283  tendoid0  41285  tendoconid  41289  tendotr  41290  cdlemk25-3  41364  cdlemk26b-3  41365  cdlemk34  41370  cdlemk36  41373  cdlemk38  41375  cdlemkid4  41394  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk19x  41403  cdlemk53  41417  cdlemk55  41421  cdlemk55u  41426  cdlemk39u  41428  cdlemk19u  41430  cdlemk56  41431  tendoex  41435  cdleml3N  41438  cdleml5N  41440  tendospcanN  41483  cdlemm10N  41578  cdlemn11pre  41670  dihord2pre  41685  dihvalcqpre  41695  dihopelvalcpre  41708  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dihord  41724  dihmeetlem1N  41750  dihglblem5apreN  41751  dihglblem3N  41755  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetbN  41763  dihmeetlem4preN  41766  dihmeetlem5  41768  dihmeetlem7N  41770  dihmeetlem10N  41776  dihmeetlem11N  41777  dihmeetlem12N  41778  dihmeetlem13N  41779  dihmeetlem15N  41781  dihmeetlem16N  41782  dihmeetlem17N  41783  dihmeetlem18N  41784  dihmeetlem19N  41785  dihmeetALTN  41787  dih1dimatlem0  41788  dihlspsnssN  41792  dihlspsnat  41793  mapdh8ad  42239  hdmap14lem14  42341  hgmapvvlem3  42385  aks6d1c6isolem1  42627  dvdsexpnn  42779  resubcan2  42834  mzprename  43195  eldioph2lem1  43206  lzunuz  43214  rencldnfi  43267  pellexlem2  43276  infmrgelbi  43324  pellfundglb  43331  pellfund14gap  43333  qirropth  43354  rmxycomplete  43363  congadd  43412  acongeq  43429  jm2.19  43439  jm2.23  43442  jm2.20nn  43443  jm2.27  43454  jm3.1  43466  aomclem6  43505  lnmepi  43531  lmhmfgsplit  43532  lmhmlnmsplit  43533  pwssplit4  43535  hbtlem2  43570  hbtlem5  43574  dgraa0p  43595  proot1hash  43641  iocunico  43657  oasubex  43732  oege1  43752  relexpxpmin  44162  brtrclfv2  44172  ntrclsiso  44512  ntrclskb  44514  ntrclsk3  44515  k0004lem3  44594  grur1cld  44677  ismnu  44706  grumnudlem  44730  suprnmpt  45622  wessf1ornlem  45633  projf1o  45644  snunioo1  45960  iccintsng  45971  lptre2pt  46086  limcleqr  46090  fnlimfvre  46120  limsupgtlem  46223  volioc  46418  iblspltprt  46419  stoweidlem19  46465  stoweidlem20  46466  stoweidlem22  46468  stoweidlem28  46474  stoweidlem34  46480  stoweidlem44  46490  stoweidlem60  46506  wallispilem3  46513  fourierdlem41  46594  fourierdlem42  46595  fourierdlem49  46601  fourierdlem51  46603  fourierdlem54  46606  fourierdlem74  46626  fourierdlem97  46649  caratheodorylem2  46973  ovnsubaddlem2  47017  hspmbllem2  47073  smflimmpt  47256  smflimsupmpt  47275  smfliminfmpt  47278  funfocofob  47538  fzopredsuc  47784  nnmul2b  47791  imasetpreimafvbijlemfv  47874  iccpartigtl  47895  lighneal  48086  oexpnegALTV  48165  oexpnegnz  48166  tgblthelfgott  48303  clnbgrgrim  48422  uhgrimgrlim  48475  gpgusgralem  48544  lidldomn1  48719  ofaddmndmap  48831  lincdifsn  48912  lincellss  48914  lincresunit3lem3  48962  islindeps2  48971  lindssnlvec  48974  fdivmptf  49029  refdivmptf  49030  rrx2linest  49230  itsclc0yqsollem1  49250  itsclc0b  49260  itsclquadb  49264  itscnhlinecirc02plem3  49272  diag1  49791  setc1onsubc  50089