Theorem simpl1 1192

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 1186	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  1249  simpl21  1252  simpl31  1255  simp1l1  1267  simp2l1  1273  simp3l1  1279  3anandirs  1474  rspc3ev  3593  2nreu  4396  predtrss  6280  frpomin  6298  f1prex  7230  cocan1  7237  weniso  7300  frrlem4  8231  frrlem10  8237  fprlem1  8242  smogt  8299  smocdmdom  8300  omeulem1  8509  nnmord  8560  nnmword  8561  naddasslem1  8622  naddasslem2  8623  difsnen  8987  enfixsn  9014  mapunen  9074  ac6sfi  9184  fipreima  9258  elfiun  9333  ordiso2  9420  wemaplem2  9452  en2eqpr  9917  indcardi  9951  fodomfi2  9970  iunfictbso  10024  infmap2  10127  cofsmo  10179  cfsmolem  10180  coftr  10183  fin23lem11  10227  fincssdom  10233  fin23lem26  10235  isf32lem9  10271  ac6num  10389  gchdomtri  10540  gchpwdom  10581  winainflem  10604  tskuni  10694  gruima  10713  gruf  10722  grudomon  10728  elnpi  10899  distrlem4pr  10937  prlem934  10944  addcan  11317  addcan2  11318  divmulass  11819  divmulasscom  11820  ltmul1a  11990  suprleub  12108  supmul1  12111  suprzcl  12572  uzsupss  12853  xleadd1a  13168  xlesubadd  13178  xmulasslem3  13201  xlemul2a  13204  xadddilem  13209  xadddi2  13212  ixxun  13277  icoshftf1o  13390  ioounsn  13393  snunioc  13396  lincmb01cmp  13411  iccf1o  13412  nn0p1elfzo  13618  fzofzim  13625  fzoopth  13678  ltexp2a  14089  leexp2  14094  ltexp2r  14096  exple1  14100  expnlbnd2  14157  fun2dmnop0  14427  ccatass  14512  swrdswrdlem  14627  ccatopth  14639  repswpfx  14708  2cshw  14736  cshimadifsn  14752  cshimadifsn0  14753  cshco  14759  repsco  14763  s2f1o  14839  limsupgre  15404  addcn2  15517  mulcn2  15519  ntrivcvgmul  15825  binomrisefac  15965  dvdsmodexp  16187  dvdsadd2b  16233  dvdsexp2im  16254  dvdsmod  16256  oexpneg  16272  sadass  16398  gcdass  16474  rplpwr  16485  lcmfunsnlem1  16564  coprmdvds2  16581  rpmulgcd2  16583  qredeq  16584  rpdvds  16587  cncongr2  16595  rpexp  16649  prmdiveq  16713  hashgcdlem  16715  odzdvds  16723  modprmn0modprm0  16735  coprimeprodsq2  16737  pythagtriplem3  16746  pcdvdsb  16797  pcgcd1  16805  qexpz  16829  pockthg  16834  vdwnnlem1  16923  0ram  16948  ramz2  16952  lubss  18436  lubun  18438  clatleglb  18441  clatglbss  18442  mrelatglb  18483  isnsgrp  18648  issubmnd  18686  ress0g  18687  mhmvlin  18726  gsumccat  18766  frmdss2  18788  submefmnd  18820  mulgneg  19022  mulgdirlem  19035  submmulg  19048  subgmulg  19070  nmzsubg  19094  ghmmulg  19157  gsmsymgreqlem1  19359  pmtrfb  19394  psgnunilem4  19426  odmodnn0  19469  odnncl  19474  odmod  19475  odmulgid  19483  odmulgeq  19486  odf1o1  19501  odf1o2  19502  odngen  19506  gexdvdsi  19512  pgpfi1  19524  odcau  19533  subgslw  19545  fislw  19554  lsmssv  19572  lsmless1x  19573  lsmless2x  19574  lsmsubm  19582  lsmmod  19604  lsmmod2  19605  efgred  19677  cntzcmn  19769  ghmplusg  19775  odadd1  19777  odadd2  19778  odadd  19779  lsmcomx  19785  gsumconst  19863  ablsimpgprmd  20046  srg1zr  20150  ring1eq0  20233  mulgass2  20244  rngisom1  20402  rhmdvdsr  20441  isabvd  20745  rmodislmodlem  20880  rmodislmod  20881  lssintcl  20915  0lmhm  20992  lmhmvsca  20997  reslmhm2b  21006  pwssplit1  21011  pwssplit3  21013  lspfixed  21083  lspsnat  21100  rnglidlrng  21202  2idlcpblrng  21226  lidldvgen  21289  xrsdsreclblem  21367  regsumsupp  21577  obselocv  21683  uvcresum  21748  frlmsslsp  21751  frlmup4  21756  lindff1  21775  f1lindf  21777  lsslindf  21785  islindf4  21793  lbslcic  21796  issubassa  21822  evlsval2  22042  psrplusgpropd  22176  coe1subfv  22208  coe1mul2  22211  mpomatmul  22390  mamutpos  22402  scmatscmide  22451  mavmulsolcl  22495  marrepcl  22508  mdetdiag  22543  mdetunilem1  22556  mdetunilem3  22558  mdetunilem7  22562  mdetunilem9  22564  mdetmul  22567  slesolinvbi  22625  m2pmfzmap  22691  pmatcollpwlem  22724  pmatcollpw  22725  mp2pm2mplem4  22753  chpdmatlem3  22784  chfacfisfcpmat  22799  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  chfacfpmmulgsum2  22809  cayhamlem1  22810  cpmidpmatlem2  22815  cpmadugsumlemB  22818  cpmadugsumlemC  22819  cpmadugsumlemF  22820  riinopn  22852  neiint  23048  topssnei  23068  restntr  23126  iscnp4  23207  cnconst2  23227  cnrest2  23230  cnprest2  23234  cnpdis  23237  cnt0  23290  cnt1  23294  cnhaus  23298  ordthauslem  23327  cncmp  23336  fiuncmp  23348  sscmp  23349  hauscmp  23351  cnconn  23366  unconn  23373  nlly2i  23420  llynlly  23421  nllyidm  23433  finlocfin  23464  ptrescn  23583  xkococnlem  23603  qtopss  23659  kqfvima  23674  r0cld  23682  ordthmeolem  23745  fbssint  23782  fmf  23889  fmss  23890  elfm  23891  rnelfmlem  23896  rnelfm  23897  fmco  23905  flimss2  23916  flimss1  23917  flimrest  23927  flftg  23940  cnpflf2  23944  cnpflf  23945  flfcnp  23948  supnfcls  23964  fclsss1  23966  fclsss2  23967  fcfnei  23979  fcfelbas  23980  cnpfcfi  23984  subgntr  24051  opnsubg  24052  cldsubg  24055  ghmcnp  24059  utop2nei  24194  neipcfilu  24239  bldisj  24342  blgt0  24343  bl2in  24344  blss2ps  24347  blss2  24348  blssps  24368  blss  24369  xmetresbl  24381  lpbl  24447  blcld  24449  stdbdbl  24461  metcnp3  24484  metcnp2  24486  txmetcnp  24491  blval2  24506  nmoix  24673  nmoeq0  24680  icoopnst  24892  iocopnst  24893  xrhmeo  24900  nmhmcn  25076  cphsqrtcl2  25142  cphsqrtcl3  25143  cfil3i  25225  caublcls  25265  bcthlem5  25284  cmetcusp1  25309  cssbn  25331  rrxcph  25348  pjth  25395  ovoliunlem2  25460  volun  25502  volsup2  25562  mbfimaopn2  25614  iblconst  25775  itgconst  25776  dvcnp2  25877  dvcnp2OLD  25878  dvcn  25879  deg1mul3le  26078  deg1tmle  26079  dvdsq1p  26124  ig1peu  26136  ig1pdvds  26141  coeid3  26201  dgrmulc  26233  efcvx  26415  tanord  26503  logdivlti  26585  logccv  26628  recxpcl  26640  cxpeq  26723  ang180  26780  isosctrlem2  26785  cxp2lim  26943  amgm  26957  muval1  27099  dvdssqf  27104  mumullem2  27146  mumul  27147  bcmono  27244  lgsfcl2  27270  lgsdilem  27291  lgsdirprm  27298  lgsdir  27299  lgsdi  27301  lgsne0  27302  padicabv  27597  nosep1o  27649  nosep2o  27650  nosepssdm  27654  nolt02olem  27662  nosupres  27675  nosupbnd1lem1  27676  nosupbnd1lem4  27679  nosupbnd1lem5  27680  nosupbnd1lem6  27681  nosupbnd2  27684  noinfres  27690  noinfbnd1lem1  27691  noinfbnd1lem4  27694  noinfbnd1lem6  27696  noinfbnd2  27699  noetasuplem3  27703  noetalem1  27709  cutbdaybnd  27791  ltslpss  27904  leslss  27905  coinitslts  27915  addsass  28001  addsdi  28151  mulsass  28162  norecdiv  28186  bdayfinbndlem1  28463  z12bdaylem  28480  brbtwn2  28978  colinearalglem1  28979  colinearalg  28983  axcgrtr  28988  axsegconlem8  28997  axsegconlem9  28998  axsegconlem10  28999  axcontlem8  29044  axcontlem10  29046  elntg2  29058  vtxdlfuhgr1v  29553  umgr2wlk  30022  erclwwlksym  30096  clwwlkfo  30125  clwwlkext2edg  30131  erclwwlknsym  30145  clwwlknon1  30172  numclwwlk2lem1  30451  numclwwlk5  30463  frgrregord13  30471  nvmul0or  30725  ipval2lem2  30779  lnomul  30835  shless  31434  shlej1  31435  pjspansn  31652  hoadddi  31878  kbmul  32030  homco2  32052  kbass2  32192  eliccelico  32857  elicoelioo  32858  iocinioc2  32859  iocinif  32861  swrdrn2  33036  xrge0adddir  33100  xrge0npcan  33102  archiabl  33280  ress1r  33315  pidlnz  33457  grplsm0l  33484  intlidl  33501  ssmxidl  33555  pstmfval  34053  fmcncfil  34088  zrhnm  34124  qqhnm  34147  measvunilem  34369  volfiniune  34387  dya2iocnrect  34438  sibfinima  34496  probun  34576  probinc  34578  cndprob01  34592  signstfvp  34728  bnj517  35041  bnj594  35068  fissorduni  35246  pconnpi1  35431  cvmsss2  35468  mrsubcv  35704  msubvrs  35754  br6  35951  br4  35952  cgrcomim  36183  cgrtriv  36196  cgrextend  36202  segconeq  36204  btwntriv2  36206  btwnintr  36213  btwnexch3  36214  btwnouttr2  36216  trisegint  36222  cgrsub  36239  cgrxfr  36249  btwnxfr  36250  lineext  36270  btwnconn1lem13  36293  btwnconn1lem14  36294  btwnconn3  36297  segcon2  36299  brsegle  36302  brsegle2  36303  segletr  36308  segleantisym  36309  seglelin  36310  outsideofeu  36325  lineunray  36341  lineelsb2  36342  ivthALT  36529  weiunpo  36659  weiunso  36660  weiunfr  36661  weiunse  36662  lindsenlbs  37812  areacirc  37910  cocanfo  37916  upixp  37926  ismtyima  38000  rrndstprj2  38028  zerdivemp1x  38144  lsatfixedN  39265  lssat  39272  eqlkr  39355  eqlkr2  39356  lkrlsp  39358  lshpkrlem4  39369  opposet  39437  cvrcon3b  39533  cvrcmp  39539  atlen0  39566  atnle  39573  atlatmstc  39575  cvlatexch3  39594  cvlsupr2  39599  hlsupr2  39643  hlrelat2  39659  cvrexchlem  39675  lnnat  39683  atcvrj2b  39688  atle  39692  atexchcvrN  39696  atbtwn  39702  athgt  39712  3dimlem3  39717  3dim1  39723  1cvratlt  39730  1cvrjat  39731  ps-1  39733  ps-2  39734  3atlem3  39741  3atlem5  39743  3atlem7  39745  llni  39764  llni2  39768  atcvrlln2  39775  llnexatN  39777  llncmp  39778  2llnmat  39780  2at0mat0  39781  lplni  39788  lplnnle2at  39797  2atnelpln  39800  lplnllnneN  39812  llncvrlpln2  39813  2lplnmN  39815  2llnmj  39816  lplncmp  39818  lplnexatN  39819  lplnexllnN  39820  2llnm3N  39825  lvoli  39831  lvoli3  39833  islvol2aN  39848  4atlem0a  39849  4atlem3  39852  4atlem3a  39853  4atlem4a  39855  4atlem4b  39856  4atlem4c  39857  4atlem4d  39858  4atlem10b  39861  4atlem11  39865  4atlem12  39868  lplncvrlvol2  39871  lvolcmp  39873  2lplnmj  39878  islinei  39996  pmapglbx  40025  linepmap  40031  lneq2at  40034  lnjatN  40036  lncvrat  40038  lncmp  40039  2llnma3r  40044  elpaddatriN  40059  elpaddat  40060  paddcom  40069  paddss1  40073  paddss2  40074  paddss12  40075  paddasslem6  40081  paddasslem7  40082  paddasslem8  40083  paddasslem9  40084  paddasslem15  40090  pmodlem2  40103  pmodl42N  40107  pmapjoin  40108  llnmod1i2  40116  2polcon4bN  40174  polcon2bN  40176  poml4N  40209  poml6N  40211  osumcllem1N  40212  osumcllem2N  40213  osumcllem11N  40222  osumclN  40223  pmapojoinN  40224  pexmidlem2N  40227  pexmidlem3N  40228  pexmidlem4N  40229  pexmidlem6N  40231  pexmidlem7N  40232  pl42lem2N  40236  pl42lem3N  40237  pl42lem4N  40238  pl42N  40239  lhpexle2lem  40265  lhpexle3lem  40267  lhpexle3  40268  lhpmcvr3  40281  lhp2at0nle  40291  lhprelat3N  40296  4atex  40332  4atex2  40333  lauteq  40351  lautco  40353  ltrncoidN  40384  ltrneq2  40404  ltrnnidn  40430  ltrnideq  40431  trlnid  40435  ltrnatlw  40439  trlnle  40442  trlval3  40443  trlval4  40444  cdlemc  40453  cdlemd5  40458  cdlemd9  40462  ltrneq3  40464  cdleme0moN  40481  cdleme20  40580  cdleme21j  40592  cdleme21  40593  cdleme27cl  40622  cdlemefrs29bpre0  40652  cdlemefs27cl  40669  cdlemefs32sn1aw  40670  cdleme43fsv1snlem  40676  cdleme32d  40700  cdleme32f  40702  cdleme32le  40703  cdleme35h2  40713  cdleme38n  40720  cdleme40m  40723  cdleme41snaw  40732  cdleme42ke  40741  cdleme17d3  40752  cdleme48fvg  40756  cdlemeg46fvcl  40762  cdlemeg46fgN  40790  cdleme48gfv1  40792  cdleme48fgv  40794  cdleme50trn3  40809  trlord  40825  ltrniotavalbN  40840  cdlemb3  40862  cdlemg6c  40876  cdlemg6  40879  cdlemg7N  40882  cdlemg8c  40885  cdlemg8  40887  cdlemg11a  40893  cdlemg11b  40898  cdlemg12e  40903  cdlemg15a  40911  cdlemg15  40912  cdlemg16  40913  cdlemg16z  40915  cdlemg16zz  40916  cdlemg17dN  40919  cdlemg18a  40934  cdlemg20  40941  cdlemg22  40943  cdlemg24  40944  cdlemg37  40945  cdlemg31d  40956  cdlemg29  40961  cdlemg33b  40963  cdlemg33  40967  cdlemg38  40971  cdlemg39  40972  cdlemg40  40973  trlco  40983  trlcone  40984  cdlemg42  40985  cdlemg44b  40988  ltrncom  40994  trljco  40996  tendococl  41028  tendoplcl  41037  tendoplcom  41038  cdlemj2  41078  cdlemj3  41079  tendoid0  41081  tendoconid  41085  tendotr  41086  cdlemk25-3  41160  cdlemk26b-3  41161  cdlemk34  41166  cdlemk36  41169  cdlemk38  41171  cdlemkid4  41190  cdlemk35s-id  41194  cdlemk39s-id  41196  cdlemk19x  41199  cdlemk53  41213  cdlemk55  41217  cdlemk55u  41222  cdlemk39u  41224  cdlemk19u  41226  cdlemk56  41227  tendoex  41231  cdleml3N  41234  cdleml5N  41236  tendospcanN  41279  cdlemm10N  41374  cdlemn11pre  41466  dihord2pre  41481  dihvalcqpre  41491  dihopelvalcpre  41504  dihord6apre  41512  dihord5b  41515  dihord5apre  41518  dihord  41520  dihmeetlem1N  41546  dihglblem5apreN  41547  dihglblem3N  41551  dihmeetlem2N  41555  dihglbcpreN  41556  dihmeetbN  41559  dihmeetlem4preN  41562  dihmeetlem5  41564  dihmeetlem7N  41566  dihmeetlem10N  41572  dihmeetlem11N  41573  dihmeetlem12N  41574  dihmeetlem13N  41575  dihmeetlem15N  41577  dihmeetlem16N  41578  dihmeetlem17N  41579  dihmeetlem18N  41580  dihmeetlem19N  41581  dihmeetALTN  41583  dih1dimatlem0  41584  dihlspsnssN  41588  dihlspsnat  41589  mapdh8ad  42035  hdmap14lem14  42137  hgmapvvlem3  42181  aks6d1c6isolem1  42424  dvdsexpnn  42584  resubcan2  42639  mzprename  42987  eldioph2lem1  42998  lzunuz  43006  rencldnfi  43059  pellexlem2  43068  infmrgelbi  43116  pellfundglb  43123  pellfund14gap  43125  qirropth  43146  rmxycomplete  43155  congadd  43204  acongeq  43221  jm2.19  43231  jm2.23  43234  jm2.20nn  43235  jm2.27  43246  jm3.1  43258  aomclem6  43297  lnmepi  43323  lmhmfgsplit  43324  lmhmlnmsplit  43325  pwssplit4  43327  hbtlem2  43362  hbtlem5  43366  dgraa0p  43387  proot1hash  43433  iocunico  43449  oasubex  43524  oege1  43544  relexpxpmin  43954  brtrclfv2  43964  ntrclsiso  44304  ntrclskb  44306  ntrclsk3  44307  k0004lem3  44386  grur1cld  44469  ismnu  44498  grumnudlem  44522  suprnmpt  45414  wessf1ornlem  45425  projf1o  45437  snunioo1  45754  iccintsng  45765  lptre2pt  45880  limcleqr  45884  fnlimfvre  45914  limsupgtlem  46017  volioc  46212  iblspltprt  46213  stoweidlem19  46259  stoweidlem20  46260  stoweidlem22  46262  stoweidlem28  46268  stoweidlem34  46274  stoweidlem44  46284  stoweidlem60  46300  wallispilem3  46307  fourierdlem41  46388  fourierdlem42  46389  fourierdlem49  46395  fourierdlem51  46397  fourierdlem54  46400  fourierdlem74  46420  fourierdlem97  46443  caratheodorylem2  46767  ovnsubaddlem2  46811  hspmbllem2  46867  smflimmpt  47050  smflimsupmpt  47069  smfliminfmpt  47072  funfocofob  47320  fzopredsuc  47565  imasetpreimafvbijlemfv  47644  iccpartigtl  47665  lighneal  47853  oexpnegALTV  47919  oexpnegnz  47920  tgblthelfgott  48057  clnbgrgrim  48176  uhgrimgrlim  48229  gpgusgralem  48298  lidldomn1  48473  ofaddmndmap  48585  lincdifsn  48666  lincellss  48668  lincresunit3lem3  48716  islindeps2  48725  lindssnlvec  48728  fdivmptf  48783  refdivmptf  48784  rrx2linest  48984  itsclc0yqsollem1  49004  itsclc0b  49014  itsclquadb  49018  itscnhlinecirc02plem3  49026  diag1  49545  setc1onsubc  49843