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  3608  2nreu  4410  predtrss  6298  frpomin  6316  f1prex  7262  cocan1  7269  weniso  7332  frrlem4  8271  frrlem10  8277  fprlem1  8282  smogt  8339  smocdmdom  8340  omeulem1  8549  nnmord  8599  nnmword  8600  naddasslem1  8661  naddasslem2  8662  difsnen  9027  enfixsn  9055  mapunen  9116  ac6sfi  9238  fipreima  9316  elfiun  9388  ordiso2  9475  wemaplem2  9507  en2eqpr  9967  indcardi  10001  fodomfi2  10020  iunfictbso  10074  infmap2  10177  cofsmo  10229  cfsmolem  10230  coftr  10233  fin23lem11  10277  fincssdom  10283  fin23lem26  10285  isf32lem9  10321  ac6num  10439  gchdomtri  10589  gchpwdom  10630  winainflem  10653  tskuni  10743  gruima  10762  gruf  10771  grudomon  10777  elnpi  10948  distrlem4pr  10986  prlem934  10993  addcan  11365  addcan2  11366  divmulass  11867  divmulasscom  11868  ltmul1a  12038  suprleub  12156  supmul1  12159  suprzcl  12621  uzsupss  12906  xleadd1a  13220  xlesubadd  13230  xmulasslem3  13253  xlemul2a  13256  xadddilem  13261  xadddi2  13264  ixxun  13329  icoshftf1o  13442  ioounsn  13445  snunioc  13448  lincmb01cmp  13463  iccf1o  13464  nn0p1elfzo  13670  fzofzim  13677  fzoopth  13730  ltexp2a  14138  leexp2  14143  ltexp2r  14145  exple1  14149  expnlbnd2  14206  fun2dmnop0  14476  ccatass  14560  swrdswrdlem  14676  ccatopth  14688  repswpfx  14757  2cshw  14785  cshimadifsn  14802  cshimadifsn0  14803  cshco  14809  repsco  14813  s2f1o  14889  limsupgre  15454  addcn2  15567  mulcn2  15569  ntrivcvgmul  15875  binomrisefac  16015  dvdsmodexp  16237  dvdsadd2b  16283  dvdsexp2im  16304  dvdsmod  16306  oexpneg  16322  sadass  16448  gcdass  16524  rplpwr  16535  lcmfunsnlem1  16614  coprmdvds2  16631  rpmulgcd2  16633  qredeq  16634  rpdvds  16637  cncongr2  16645  rpexp  16699  prmdiveq  16763  hashgcdlem  16765  odzdvds  16773  modprmn0modprm0  16785  coprimeprodsq2  16787  pythagtriplem3  16796  pcdvdsb  16847  pcgcd1  16855  qexpz  16879  pockthg  16884  vdwnnlem1  16973  0ram  16998  ramz2  17002  lubss  18479  lubun  18481  clatleglb  18484  clatglbss  18485  mrelatglb  18526  isnsgrp  18657  issubmnd  18695  ress0g  18696  mhmvlin  18735  gsumccat  18775  frmdss2  18797  submefmnd  18829  mulgneg  19031  mulgdirlem  19044  submmulg  19057  subgmulg  19079  nmzsubg  19104  ghmmulg  19167  gsmsymgreqlem1  19367  pmtrfb  19402  psgnunilem4  19434  odmodnn0  19477  odnncl  19482  odmod  19483  odmulgid  19491  odmulgeq  19494  odf1o1  19509  odf1o2  19510  odngen  19514  gexdvdsi  19520  pgpfi1  19532  odcau  19541  subgslw  19553  fislw  19562  lsmssv  19580  lsmless1x  19581  lsmless2x  19582  lsmsubm  19590  lsmmod  19612  lsmmod2  19613  efgred  19685  cntzcmn  19777  ghmplusg  19783  odadd1  19785  odadd2  19786  odadd  19787  lsmcomx  19793  gsumconst  19871  ablsimpgprmd  20054  srg1zr  20131  ring1eq0  20214  mulgass2  20225  rngisom1  20382  rhmdvdsr  20424  isabvd  20728  rmodislmodlem  20842  rmodislmod  20843  lssintcl  20877  0lmhm  20954  lmhmvsca  20959  reslmhm2b  20968  pwssplit1  20973  pwssplit3  20975  lspfixed  21045  lspsnat  21062  rnglidlrng  21164  2idlcpblrng  21188  lidldvgen  21251  xrsdsreclblem  21336  regsumsupp  21538  obselocv  21644  uvcresum  21709  frlmsslsp  21712  frlmup4  21717  lindff1  21736  f1lindf  21738  lsslindf  21746  islindf4  21754  lbslcic  21757  issubassa  21783  evlsval2  22001  psrplusgpropd  22127  coe1subfv  22159  coe1mul2  22162  mpomatmul  22340  mamutpos  22352  scmatscmide  22401  mavmulsolcl  22445  marrepcl  22458  mdetdiag  22493  mdetunilem1  22506  mdetunilem3  22508  mdetunilem7  22512  mdetunilem9  22514  mdetmul  22517  slesolinvbi  22575  m2pmfzmap  22641  pmatcollpwlem  22674  pmatcollpw  22675  mp2pm2mplem4  22703  chpdmatlem3  22734  chfacfisfcpmat  22749  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  chfacfpmmulgsum2  22759  cayhamlem1  22760  cpmidpmatlem2  22765  cpmadugsumlemB  22768  cpmadugsumlemC  22769  cpmadugsumlemF  22770  riinopn  22802  neiint  22998  topssnei  23018  restntr  23076  iscnp4  23157  cnconst2  23177  cnrest2  23180  cnprest2  23184  cnpdis  23187  cnt0  23240  cnt1  23244  cnhaus  23248  ordthauslem  23277  cncmp  23286  fiuncmp  23298  sscmp  23299  hauscmp  23301  cnconn  23316  unconn  23323  nlly2i  23370  llynlly  23371  nllyidm  23383  finlocfin  23414  ptrescn  23533  xkococnlem  23553  qtopss  23609  kqfvima  23624  r0cld  23632  ordthmeolem  23695  fbssint  23732  fmf  23839  fmss  23840  elfm  23841  rnelfmlem  23846  rnelfm  23847  fmco  23855  flimss2  23866  flimss1  23867  flimrest  23877  flftg  23890  cnpflf2  23894  cnpflf  23895  flfcnp  23898  supnfcls  23914  fclsss1  23916  fclsss2  23917  fcfnei  23929  fcfelbas  23930  cnpfcfi  23934  subgntr  24001  opnsubg  24002  cldsubg  24005  ghmcnp  24009  utop2nei  24145  neipcfilu  24190  bldisj  24293  blgt0  24294  bl2in  24295  blss2ps  24298  blss2  24299  blssps  24319  blss  24320  xmetresbl  24332  lpbl  24398  blcld  24400  stdbdbl  24412  metcnp3  24435  metcnp2  24437  txmetcnp  24442  blval2  24457  nmoix  24624  nmoeq0  24631  icoopnst  24843  iocopnst  24844  xrhmeo  24851  nmhmcn  25027  cphsqrtcl2  25093  cphsqrtcl3  25094  cfil3i  25176  caublcls  25216  bcthlem5  25235  cmetcusp1  25260  cssbn  25282  rrxcph  25299  pjth  25346  ovoliunlem2  25411  volun  25453  volsup2  25513  mbfimaopn2  25565  iblconst  25726  itgconst  25727  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  deg1mul3le  26029  deg1tmle  26030  dvdsq1p  26075  ig1peu  26087  ig1pdvds  26092  coeid3  26152  dgrmulc  26184  efcvx  26366  tanord  26454  logdivlti  26536  logccv  26579  recxpcl  26591  cxpeq  26674  ang180  26731  isosctrlem2  26736  cxp2lim  26894  amgm  26908  muval1  27050  dvdssqf  27055  mumullem2  27097  mumul  27098  bcmono  27195  lgsfcl2  27221  lgsdilem  27242  lgsdirprm  27249  lgsdir  27250  lgsdi  27252  lgsne0  27253  padicabv  27548  nosep1o  27600  nosep2o  27601  nosepssdm  27605  nolt02olem  27613  nosupres  27626  nosupbnd1lem1  27627  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  nosupbnd2  27635  noinfres  27641  noinfbnd1lem1  27642  noinfbnd1lem4  27645  noinfbnd1lem6  27647  noinfbnd2  27650  noetasuplem3  27654  noetalem1  27660  scutbdaybnd  27734  sltlpss  27826  slelss  27827  coinitsslt  27834  addsass  27919  addsdi  28065  mulsass  28076  norecdiv  28100  brbtwn2  28839  colinearalglem1  28840  colinearalg  28844  axcgrtr  28849  axsegconlem8  28858  axsegconlem9  28859  axsegconlem10  28860  axcontlem8  28905  axcontlem10  28907  elntg2  28919  vtxdlfuhgr1v  29414  umgr2wlk  29886  erclwwlksym  29957  clwwlkfo  29986  clwwlkext2edg  29992  erclwwlknsym  30006  clwwlknon1  30033  numclwwlk2lem1  30312  numclwwlk5  30324  frgrregord13  30332  nvmul0or  30586  ipval2lem2  30640  lnomul  30696  shless  31295  shlej1  31296  pjspansn  31513  hoadddi  31739  kbmul  31891  homco2  31913  kbass2  32053  eliccelico  32707  elicoelioo  32708  iocinioc2  32709  iocinif  32711  swrdrn2  32883  xrge0adddir  32966  xrge0npcan  32968  archiabl  33159  ress1r  33192  pidlnz  33354  grplsm0l  33381  intlidl  33398  ssmxidl  33452  pstmfval  33893  fmcncfil  33928  zrhnm  33964  qqhnm  33987  measvunilem  34209  volfiniune  34227  dya2iocnrect  34279  sibfinima  34337  probun  34417  probinc  34419  cndprob01  34433  signstfvp  34569  bnj517  34882  bnj594  34909  pconnpi1  35231  cvmsss2  35268  mrsubcv  35504  msubvrs  35554  br6  35751  br4  35752  cgrcomim  35984  cgrtriv  35997  cgrextend  36003  segconeq  36005  btwntriv2  36007  btwnintr  36014  btwnexch3  36015  btwnouttr2  36017  trisegint  36023  cgrsub  36040  cgrxfr  36050  btwnxfr  36051  lineext  36071  btwnconn1lem13  36094  btwnconn1lem14  36095  btwnconn3  36098  segcon2  36100  brsegle  36103  brsegle2  36104  segletr  36109  segleantisym  36110  seglelin  36111  outsideofeu  36126  lineunray  36142  lineelsb2  36143  ivthALT  36330  weiunpo  36460  weiunso  36461  weiunfr  36462  weiunse  36463  lindsenlbs  37616  areacirc  37714  cocanfo  37720  upixp  37730  ismtyima  37804  rrndstprj2  37832  zerdivemp1x  37948  lsatfixedN  39009  lssat  39016  eqlkr  39099  eqlkr2  39100  lkrlsp  39102  lshpkrlem4  39113  opposet  39181  cvrcon3b  39277  cvrcmp  39283  atlen0  39310  atnle  39317  atlatmstc  39319  cvlatexch3  39338  cvlsupr2  39343  hlsupr2  39388  hlrelat2  39404  cvrexchlem  39420  lnnat  39428  atcvrj2b  39433  atle  39437  atexchcvrN  39441  atbtwn  39447  athgt  39457  3dimlem3  39462  3dim1  39468  1cvratlt  39475  1cvrjat  39476  ps-1  39478  ps-2  39479  3atlem3  39486  3atlem5  39488  3atlem7  39490  llni  39509  llni2  39513  atcvrlln2  39520  llnexatN  39522  llncmp  39523  2llnmat  39525  2at0mat0  39526  lplni  39533  lplnnle2at  39542  2atnelpln  39545  lplnllnneN  39557  llncvrlpln2  39558  2lplnmN  39560  2llnmj  39561  lplncmp  39563  lplnexatN  39564  lplnexllnN  39565  2llnm3N  39570  lvoli  39576  lvoli3  39578  islvol2aN  39593  4atlem0a  39594  4atlem3  39597  4atlem3a  39598  4atlem4a  39600  4atlem4b  39601  4atlem4c  39602  4atlem4d  39603  4atlem10b  39606  4atlem11  39610  4atlem12  39613  lplncvrlvol2  39616  lvolcmp  39618  2lplnmj  39623  islinei  39741  pmapglbx  39770  linepmap  39776  lneq2at  39779  lnjatN  39781  lncvrat  39783  lncmp  39784  2llnma3r  39789  elpaddatriN  39804  elpaddat  39805  paddcom  39814  paddss1  39818  paddss2  39819  paddss12  39820  paddasslem6  39826  paddasslem7  39827  paddasslem8  39828  paddasslem9  39829  paddasslem15  39835  pmodlem2  39848  pmodl42N  39852  pmapjoin  39853  llnmod1i2  39861  2polcon4bN  39919  polcon2bN  39921  poml4N  39954  poml6N  39956  osumcllem1N  39957  osumcllem2N  39958  osumcllem11N  39967  osumclN  39968  pmapojoinN  39969  pexmidlem2N  39972  pexmidlem3N  39973  pexmidlem4N  39974  pexmidlem6N  39976  pexmidlem7N  39977  pl42lem2N  39981  pl42lem3N  39982  pl42lem4N  39983  pl42N  39984  lhpexle2lem  40010  lhpexle3lem  40012  lhpexle3  40013  lhpmcvr3  40026  lhp2at0nle  40036  lhprelat3N  40041  4atex  40077  4atex2  40078  lauteq  40096  lautco  40098  ltrncoidN  40129  ltrneq2  40149  ltrnnidn  40175  ltrnideq  40176  trlnid  40180  ltrnatlw  40184  trlnle  40187  trlval3  40188  trlval4  40189  cdlemc  40198  cdlemd5  40203  cdlemd9  40207  ltrneq3  40209  cdleme0moN  40226  cdleme20  40325  cdleme21j  40337  cdleme21  40338  cdleme27cl  40367  cdlemefrs29bpre0  40397  cdlemefs27cl  40414  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme32d  40445  cdleme32f  40447  cdleme32le  40448  cdleme35h2  40458  cdleme38n  40465  cdleme40m  40468  cdleme41snaw  40477  cdleme42ke  40486  cdleme17d3  40497  cdleme48fvg  40501  cdlemeg46fvcl  40507  cdlemeg46fgN  40535  cdleme48gfv1  40537  cdleme48fgv  40539  cdleme50trn3  40554  trlord  40570  ltrniotavalbN  40585  cdlemb3  40607  cdlemg6c  40621  cdlemg6  40624  cdlemg7N  40627  cdlemg8c  40630  cdlemg8  40632  cdlemg11a  40638  cdlemg11b  40643  cdlemg12e  40648  cdlemg15a  40656  cdlemg15  40657  cdlemg16  40658  cdlemg16z  40660  cdlemg16zz  40661  cdlemg17dN  40664  cdlemg18a  40679  cdlemg20  40686  cdlemg22  40688  cdlemg24  40689  cdlemg37  40690  cdlemg31d  40701  cdlemg29  40706  cdlemg33b  40708  cdlemg33  40712  cdlemg38  40716  cdlemg39  40717  cdlemg40  40718  trlco  40728  trlcone  40729  cdlemg42  40730  cdlemg44b  40733  ltrncom  40739  trljco  40741  tendococl  40773  tendoplcl  40782  tendoplcom  40783  cdlemj2  40823  cdlemj3  40824  tendoid0  40826  tendoconid  40830  tendotr  40831  cdlemk25-3  40905  cdlemk26b-3  40906  cdlemk34  40911  cdlemk36  40914  cdlemk38  40916  cdlemkid4  40935  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk19x  40944  cdlemk53  40958  cdlemk55  40962  cdlemk55u  40967  cdlemk39u  40969  cdlemk19u  40971  cdlemk56  40972  tendoex  40976  cdleml3N  40979  cdleml5N  40981  tendospcanN  41024  cdlemm10N  41119  cdlemn11pre  41211  dihord2pre  41226  dihvalcqpre  41236  dihopelvalcpre  41249  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihord  41265  dihmeetlem1N  41291  dihglblem5apreN  41292  dihglblem3N  41296  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetbN  41304  dihmeetlem4preN  41307  dihmeetlem5  41309  dihmeetlem7N  41311  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem12N  41319  dihmeetlem13N  41320  dihmeetlem15N  41322  dihmeetlem16N  41323  dihmeetlem17N  41324  dihmeetlem18N  41325  dihmeetlem19N  41326  dihmeetALTN  41328  dih1dimatlem0  41329  dihlspsnssN  41333  dihlspsnat  41334  mapdh8ad  41780  hdmap14lem14  41882  hgmapvvlem3  41926  aks6d1c6isolem1  42169  dvdsexpnn  42328  resubcan2  42383  mzprename  42744  eldioph2lem1  42755  lzunuz  42763  rencldnfi  42816  pellexlem2  42825  infmrgelbi  42873  pellfundglb  42880  pellfund14gap  42882  qirropth  42903  rmxycomplete  42913  congadd  42962  acongeq  42979  jm2.19  42989  jm2.23  42992  jm2.20nn  42993  jm2.27  43004  jm3.1  43016  aomclem6  43055  lnmepi  43081  lmhmfgsplit  43082  lmhmlnmsplit  43083  pwssplit4  43085  hbtlem2  43120  hbtlem5  43124  dgraa0p  43145  proot1hash  43191  iocunico  43207  oasubex  43282  oege1  43302  relexpxpmin  43713  brtrclfv2  43723  ntrclsiso  44063  ntrclskb  44065  ntrclsk3  44066  k0004lem3  44145  grur1cld  44228  ismnu  44257  grumnudlem  44281  suprnmpt  45175  wessf1ornlem  45186  projf1o  45198  snunioo1  45517  iccintsng  45528  lptre2pt  45645  limcleqr  45649  fnlimfvre  45679  limsupgtlem  45782  volioc  45977  iblspltprt  45978  stoweidlem19  46024  stoweidlem20  46025  stoweidlem22  46027  stoweidlem28  46033  stoweidlem34  46039  stoweidlem44  46049  stoweidlem60  46065  wallispilem3  46072  fourierdlem41  46153  fourierdlem42  46154  fourierdlem49  46160  fourierdlem51  46162  fourierdlem54  46165  fourierdlem74  46185  fourierdlem97  46208  caratheodorylem2  46532  ovnsubaddlem2  46576  hspmbllem2  46632  smflimmpt  46815  smflimsupmpt  46834  smfliminfmpt  46837  funfocofob  47083  fzopredsuc  47328  imasetpreimafvbijlemfv  47407  iccpartigtl  47428  lighneal  47616  oexpnegALTV  47682  oexpnegnz  47683  tgblthelfgott  47820  clnbgrgrim  47938  uhgrimgrlim  47990  gpgusgralem  48051  lidldomn1  48223  ofaddmndmap  48335  lincdifsn  48417  lincellss  48419  lincresunit3lem3  48467  islindeps2  48476  lindssnlvec  48479  fdivmptf  48534  refdivmptf  48535  rrx2linest  48735  itsclc0yqsollem1  48755  itsclc0b  48765  itsclquadb  48769  itscnhlinecirc02plem3  48777  diag1  49297  setc1onsubc  49595