Theorem simpl1 1208

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl11  1265  simpl21  1268  simpl31  1271  simp1l1  1283  simp2l1  1289  simp3l1  1295  3anandirs  1496  rspc3ev  3601  2nreu  4401  predtrss  6313  frpomin  6331  f1prex  7272  cocan1  7279  weniso  7342  frrlem4  8274  frrlem10  8280  fprlem1  8285  smogt  8342  smocdmdom  8343  omeulem1  8555  nnmord  8606  nnmword  8607  naddasslem1  8669  naddasslem2  8670  difsnen  9035  enfixsn  9062  mapunen  9122  ac6sfi  9232  fipreima  9303  elfiun  9378  ordiso2  9465  wemaplem2  9497  en2eqpr  9979  indcardi  10013  fodomfi2  10032  iunfictbso  10086  infmap2  10188  cofsmo  10241  cfsmolem  10242  coftr  10245  fin23lem11  10289  fincssdom  10295  fin23lem26  10297  isf32lem9  10333  ac6num  10451  gchdomtri  10602  gchpwdom  10643  winainflem  10666  tskuni  10756  gruima  10775  gruf  10784  grudomon  10790  elnpi  10961  distrlem4pr  10999  prlem934  11006  addcan  11382  addcan2  11383  divmulass  11883  divmulasscom  11884  ltmul1a  12055  suprleub  12172  supmul1  12175  suprzcl  12667  uzsupss  12955  xleadd1a  13270  xlesubadd  13280  xmulasslem3  13303  xlemul2a  13306  xadddilem  13311  xadddi2  13314  ixxun  13379  icoshftf1o  13492  ioounsn  13495  snunioc  13498  lincmb01cmp  13513  iccf1o  13514  nn0p1elfzo  13722  fzofzim  13729  fzoopth  13782  ltexp2a  14193  leexp2  14198  ltexp2r  14200  exple1  14204  expnlbnd2  14261  fun2dmnop0  14531  ccatass  14616  swrdswrdlem  14731  ccatopth  14743  repswpfx  14812  2cshw  14840  cshimadifsn  14856  cshimadifsn0  14857  cshco  14863  repsco  14867  s2f1o  14943  limsupgre  15522  addcn2  15635  mulcn2  15637  ntrivcvgmul  15946  binomrisefac  16086  dvdsmodexp  16308  dvdsadd2b  16354  dvdsexp2im  16375  dvdsmod  16377  oexpneg  16393  sadass  16519  gcdass  16595  rplpwr  16606  lcmfunsnlem1  16685  coprmdvds2  16702  rpmulgcd2  16704  qredeq  16705  rpdvds  16708  cncongr2  16716  rpexp  16771  prmdiveq  16835  hashgcdlem  16837  odzdvds  16845  modprmn0modprm0  16857  coprimeprodsq2  16859  pythagtriplem3  16868  pcdvdsb  16919  pcgcd1  16927  qexpz  16951  pockthg  16956  vdwnnlem1  17045  0ram  17070  ramz2  17074  lubss  18559  lubun  18561  clatleglb  18564  clatglbss  18565  mrelatglb  18606  isnsgrp  18771  issubmnd  18809  ress0g  18810  mhmvlin  18849  gsumccat  18890  frmdss2  18912  submefmnd  18944  mulgneg  19149  mulgdirlem  19162  submmulg  19175  subgmulg  19198  nmzsubg  19222  ghmmulg  19289  gsmsymgreqlem1  19491  pmtrfb  19526  psgnunilem4  19558  odmodnn0  19601  odnncl  19606  odmod  19607  odmulgid  19615  odmulgeq  19618  odf1o1  19633  odf1o2  19634  odngen  19638  gexdvdsi  19644  pgpfi1  19656  odcau  19665  subgslw  19677  fislw  19686  lsmssv  19704  lsmless1x  19705  lsmless2x  19706  lsmsubm  19714  lsmmod  19736  lsmmod2  19737  efgred  19809  cntzcmn  19901  ghmplusg  19907  odadd1  19909  odadd2  19910  odadd  19911  lsmcomx  19917  gsumconst  19995  ablsimpgprmd  20178  ring1eq0  20372  mulgass2  20383  rngisom1  20539  rhmdvdsr  20582  isabvd  20884  rmodislmodlem  21019  rmodislmod  21020  lssintcl  21054  0lmhm  21130  lmhmvsca  21135  reslmhm2b  21144  pwssplit1  21149  pwssplit3  21151  lspfixed  21221  lspsnat  21238  unichnlidl  21331  rnglidlrng  21346  2idlcpblrng  21372  lidldvgen  21462  xrsdsreclblem  21523  regsumsupp  21732  obselocv  21838  uvcresum  21903  frlmsslsp  21906  frlmup4  21911  lindff1  21930  f1lindf  21932  lsslindf  21940  islindf4  21948  lbslcic  21951  issubassa  21977  evlsval2  22198  psrplusgpropd  22355  coe1subfv  22387  coe1mul2  22390  mpomatmul  22564  mamutpos  22576  scmatscmide  22625  mavmulsolcl  22669  marrepcl  22682  mdetdiag  22717  mdetunilem1  22730  mdetunilem3  22732  mdetunilem7  22736  mdetunilem9  22738  mdetmul  22741  slesolinvbi  22799  m2pmfzmap  22865  pmatcollpwlem  22898  pmatcollpw  22899  mp2pm2mplem4  22927  chpdmatlem3  22958  chfacfisfcpmat  22973  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  chfacfpmmulgsum2  22983  cayhamlem1  22984  cpmidpmatlem2  22989  cpmadugsumlemB  22992  cpmadugsumlemC  22993  cpmadugsumlemF  22994  riinopn  23026  neiint  23222  topssnei  23242  restntr  23300  iscnp4  23381  cnconst2  23401  cnrest2  23404  cnprest2  23408  cnpdis  23411  cnt0  23464  cnt1  23468  cnhaus  23472  ordthauslem  23501  cncmp  23510  fiuncmp  23522  sscmp  23523  hauscmp  23525  cnconn  23540  unconn  23547  nlly2i  23594  llynlly  23595  nllyidm  23607  finlocfin  23638  ptrescn  23757  xkococnlem  23777  qtopss  23833  kqfvima  23848  r0cld  23856  ordthmeolem  23919  fbssint  23956  fmf  24063  fmss  24064  elfm  24065  rnelfmlem  24070  rnelfm  24071  fmco  24079  flimss2  24090  flimss1  24091  flimrest  24101  flftg  24114  cnpflf2  24118  cnpflf  24119  flfcnp  24122  supnfcls  24138  fclsss1  24140  fclsss2  24141  fcfnei  24153  fcfelbas  24154  cnpfcfi  24158  subgntr  24225  opnsubg  24226  cldsubg  24229  ghmcnp  24233  utop2nei  24368  neipcfilu  24413  bldisj  24516  blgt0  24517  bl2in  24518  blss2ps  24521  blss2  24522  blssps  24542  blss  24543  xmetresbl  24555  lpbl  24621  blcld  24623  stdbdbl  24635  metcnp3  24658  metcnp2  24660  txmetcnp  24665  blval2  24680  nmoix  24847  nmoeq0  24854  icoopnst  25059  iocopnst  25060  xrhmeo  25066  nmhmcn  25240  cphsqrtcl2  25306  cphsqrtcl3  25307  cfil3i  25389  caublcls  25429  bcthlem5  25448  cmetcusp1  25473  cssbn  25495  rrxcph  25512  pjth  25559  ovoliunlem2  25623  volun  25665  volsup2  25725  mbfimaopn2  25777  iblconst  25938  itgconst  25939  dvcnp2  26040  dvcn  26041  deg1mul3le  26235  deg1tmle  26236  dvdsq1p  26281  ig1peu  26293  ig1pdvds  26298  coeid3  26358  dgrmulc  26389  efcvx  26570  tanord  26661  logdivlti  26743  logccv  26786  recxpcl  26798  cxpeq  26880  ang180  26937  isosctrlem2  26942  cxp2lim  27099  amgm  27113  muval1  27255  dvdssqf  27260  mumullem2  27302  mumul  27303  bcmono  27399  lgsfcl2  27425  lgsdilem  27446  lgsdirprm  27453  lgsdir  27454  lgsdi  27456  lgsne0  27457  padicabv  27752  nosep1o  27803  nosep2o  27804  nosepssdm  27808  nolt02olem  27816  nosupres  27829  nosupbnd1lem1  27830  nosupbnd1lem4  27833  nosupbnd1lem5  27834  nosupbnd1lem6  27835  nosupbnd2  27838  noinfres  27844  noinfbnd1lem1  27845  noinfbnd1lem4  27848  noinfbnd1lem6  27850  noinfbnd2  27853  noetasuplem3  27857  noetalem1  27863  cutbdaybnd  27946  ltslpss  28059  leslss  28060  coinitslts  28070  addsass  28156  addsdi  28306  mulsass  28317  norecdiv  28341  bdayfinbndlem1  28618  z12bdaylem  28635  brbtwn2  29164  colinearalglem1  29165  colinearalg  29169  axcgrtr  29174  axsegconlem8  29183  axsegconlem9  29184  axsegconlem10  29185  axcontlem8  29230  axcontlem10  29232  elntg2  29244  vtxdlfuhgr1v  29738  umgr2wlk  30207  erclwwlksym  30281  clwwlkfo  30310  clwwlkext2edg  30316  erclwwlknsym  30330  clwwlknon1  30357  numclwwlk2lem1  30636  numclwwlk5  30648  frgrregord13  30656  nvmul0or  30911  ipval2lem2  30965  lnomul  31021  shless  31620  shlej1  31621  pjspansn  31838  hoadddi  32064  kbmul  32216  homco2  32238  kbass2  32378  eliccelico  33034  elicoelioo  33035  iocinioc2  33036  iocinif  33038  swrdrn2  33187  xrge0adddir  33251  xrge0npcan  33253  archiabl  33431  ress1r  33465  pidlnz  33605  grplsm0l  33628  intlidl  33644  ssmxidl  33674  pstmfval  34203  fmcncfil  34238  zrhnm  34274  qqhnm  34297  measvunilem  34519  volfiniune  34537  dya2iocnrect  34588  sibfinima  34646  probun  34726  probinc  34728  cndprob01  34742  signstfvp  34875  bnj517  35190  bnj594  35217  fissorduni  35395  pconnpi1  35600  cvmsss2  35637  mrsubcv  35873  msubvrs  35923  br6  36120  br4  36121  cgrcomim  36352  cgrtriv  36365  cgrextend  36371  segconeq  36373  btwntriv2  36375  btwnintr  36382  btwnexch3  36383  btwnouttr2  36385  trisegint  36391  cgrsub  36408  cgrxfr  36418  btwnxfr  36419  lineext  36439  btwnconn1lem13  36462  btwnconn1lem14  36463  btwnconn3  36466  segcon2  36468  brsegle  36471  brsegle2  36472  segletr  36477  segleantisym  36478  seglelin  36479  outsideofeu  36494  lineunray  36510  lineelsb2  36511  ivthALT  36708  weiunpo  36838  weiunso  36839  weiunfr  36840  weiunse  36841  lindsenlbs  38126  areacirc  38224  cocanfo  38230  upixp  38240  ismtyima  38314  rrndstprj2  38342  zerdivemp1x  38458  lsatfixedN  39645  lssat  39652  eqlkr  39735  eqlkr2  39736  lkrlsp  39738  lshpkrlem4  39749  opposet  39817  cvrcon3b  39913  cvrcmp  39919  atlen0  39946  atnle  39953  atlatmstc  39955  cvlatexch3  39974  cvlsupr2  39979  hlsupr2  40023  hlrelat2  40039  cvrexchlem  40055  lnnat  40063  atcvrj2b  40068  atle  40072  atexchcvrN  40076  atbtwn  40082  athgt  40092  3dimlem3  40097  3dim1  40103  1cvratlt  40110  1cvrjat  40111  ps-1  40113  ps-2  40114  3atlem3  40121  3atlem5  40123  3atlem7  40125  llni  40144  llni2  40148  atcvrlln2  40155  llnexatN  40157  llncmp  40158  2llnmat  40160  2at0mat0  40161  lplni  40168  lplnnle2at  40177  2atnelpln  40180  lplnllnneN  40192  llncvrlpln2  40193  2lplnmN  40195  2llnmj  40196  lplncmp  40198  lplnexatN  40199  lplnexllnN  40200  2llnm3N  40205  lvoli  40211  lvoli3  40213  islvol2aN  40228  4atlem0a  40229  4atlem3  40232  4atlem3a  40233  4atlem4a  40235  4atlem4b  40236  4atlem4c  40237  4atlem4d  40238  4atlem10b  40241  4atlem11  40245  4atlem12  40248  lplncvrlvol2  40251  lvolcmp  40253  2lplnmj  40258  islinei  40376  pmapglbx  40405  linepmap  40411  lneq2at  40414  lnjatN  40416  lncvrat  40418  lncmp  40419  2llnma3r  40424  elpaddatriN  40439  elpaddat  40440  paddcom  40449  paddss1  40453  paddss2  40454  paddss12  40455  paddasslem6  40461  paddasslem7  40462  paddasslem8  40463  paddasslem9  40464  paddasslem15  40470  pmodlem2  40483  pmodl42N  40487  pmapjoin  40488  llnmod1i2  40496  2polcon4bN  40554  polcon2bN  40556  poml4N  40589  poml6N  40591  osumcllem1N  40592  osumcllem2N  40593  osumcllem11N  40602  osumclN  40603  pmapojoinN  40604  pexmidlem2N  40607  pexmidlem3N  40608  pexmidlem4N  40609  pexmidlem6N  40611  pexmidlem7N  40612  pl42lem2N  40616  pl42lem3N  40617  pl42lem4N  40618  pl42N  40619  lhpexle2lem  40645  lhpexle3lem  40647  lhpexle3  40648  lhpmcvr3  40661  lhp2at0nle  40671  lhprelat3N  40676  4atex  40712  4atex2  40713  lauteq  40731  lautco  40733  ltrncoidN  40764  ltrneq2  40784  ltrnnidn  40810  ltrnideq  40811  trlnid  40815  ltrnatlw  40819  trlnle  40822  trlval3  40823  trlval4  40824  cdlemc  40833  cdlemd5  40838  cdlemd9  40842  ltrneq3  40844  cdleme0moN  40861  cdleme20  40960  cdleme21j  40972  cdleme21  40973  cdleme27cl  41002  cdlemefrs29bpre0  41032  cdlemefs27cl  41049  cdlemefs32sn1aw  41050  cdleme43fsv1snlem  41056  cdleme32d  41080  cdleme32f  41082  cdleme32le  41083  cdleme35h2  41093  cdleme38n  41100  cdleme40m  41103  cdleme41snaw  41112  cdleme42ke  41121  cdleme17d3  41132  cdleme48fvg  41136  cdlemeg46fvcl  41142  cdlemeg46fgN  41170  cdleme48gfv1  41172  cdleme48fgv  41174  cdleme50trn3  41189  trlord  41205  ltrniotavalbN  41220  cdlemb3  41242  cdlemg6c  41256  cdlemg6  41259  cdlemg7N  41262  cdlemg8c  41265  cdlemg8  41267  cdlemg11a  41273  cdlemg11b  41278  cdlemg12e  41283  cdlemg15a  41291  cdlemg15  41292  cdlemg16  41293  cdlemg16z  41295  cdlemg16zz  41296  cdlemg17dN  41299  cdlemg18a  41314  cdlemg20  41321  cdlemg22  41323  cdlemg24  41324  cdlemg37  41325  cdlemg31d  41336  cdlemg29  41341  cdlemg33b  41343  cdlemg33  41347  cdlemg38  41351  cdlemg39  41352  cdlemg40  41353  trlco  41363  trlcone  41364  cdlemg42  41365  cdlemg44b  41368  ltrncom  41374  trljco  41376  tendococl  41408  tendoplcl  41417  tendoplcom  41418  cdlemj2  41458  cdlemj3  41459  tendoid0  41461  tendoconid  41465  tendotr  41466  cdlemk25-3  41540  cdlemk26b-3  41541  cdlemk34  41546  cdlemk36  41549  cdlemk38  41551  cdlemkid4  41570  cdlemk35s-id  41574  cdlemk39s-id  41576  cdlemk19x  41579  cdlemk53  41593  cdlemk55  41597  cdlemk55u  41602  cdlemk39u  41604  cdlemk19u  41606  cdlemk56  41607  tendoex  41611  cdleml3N  41614  cdleml5N  41616  tendospcanN  41659  cdlemm10N  41754  cdlemn11pre  41846  dihord2pre  41861  dihvalcqpre  41871  dihopelvalcpre  41884  dihord6apre  41892  dihord5b  41895  dihord5apre  41898  dihord  41900  dihmeetlem1N  41926  dihglblem5apreN  41927  dihglblem3N  41931  dihmeetlem2N  41935  dihglbcpreN  41936  dihmeetbN  41939  dihmeetlem4preN  41942  dihmeetlem5  41944  dihmeetlem7N  41946  dihmeetlem10N  41952  dihmeetlem11N  41953  dihmeetlem12N  41954  dihmeetlem13N  41955  dihmeetlem15N  41957  dihmeetlem16N  41958  dihmeetlem17N  41959  dihmeetlem18N  41960  dihmeetlem19N  41961  dihmeetALTN  41963  dih1dimatlem0  41964  dihlspsnssN  41968  dihlspsnat  41969  mapdh8ad  42415  hdmap14lem14  42517  hgmapvvlem3  42561  aks6d1c6isolem1  42803  dvdsexpnn  42954  resubcan2  43009  mzprename  43342  eldioph2lem1  43353  lzunuz  43361  rencldnfi  43410  pellexlem2  43419  infmrgelbi  43467  pellfundglb  43474  pellfund14gap  43476  qirropth  43497  rmxycomplete  43506  congadd  43555  acongeq  43572  jm2.19  43582  jm2.23  43585  jm2.20nn  43586  jm2.27  43597  jm3.1  43609  aomclem6  43648  lnmepi  43674  lmhmfgsplit  43675  lmhmlnmsplit  43676  pwssplit4  43678  hbtlem2  43713  hbtlem5  43717  dgraa0p  43738  proot1hash  43784  iocunico  43800  oasubex  43875  oege1  43895  relexpxpmin  44305  brtrclfv2  44315  ntrclsiso  44655  ntrclskb  44657  ntrclsk3  44658  k0004lem3  44737  grur1cld  44820  ismnu  44835  grumnudlem  44859  suprnmpt  45750  wessf1ornlem  45761  projf1o  45772  snunioo1  46086  iccintsng  46097  lptre2pt  46212  limcleqr  46216  fnlimfvre  46246  limsupgtlem  46349  volioc  46544  iblspltprt  46545  stoweidlem19  46591  stoweidlem20  46592  stoweidlem22  46594  stoweidlem28  46600  stoweidlem34  46606  stoweidlem44  46616  stoweidlem60  46632  wallispilem3  46639  fourierdlem41  46720  fourierdlem42  46721  fourierdlem49  46727  fourierdlem51  46729  fourierdlem54  46732  fourierdlem74  46752  fourierdlem97  46775  caratheodorylem2  47099  ovnsubaddlem2  47143  hspmbllem2  47199  smflimmpt  47382  smflimsupmpt  47401  smfliminfmpt  47404  funfocofob  47670  fzopredsuc  47916  nnmul2b  47923  imasetpreimafvbijlemfv  48006  iccpartigtl  48027  lighneal  48218  oexpnegALTV  48297  oexpnegnz  48298  tgblthelfgott  48435  clnbgrgrim  48554  uhgrimgrlim  48607  gpgusgralem  48676  lidldomn1  48851  ofaddmndmap  48974  lincdifsn  49055  lincellss  49057  lincresunit3lem3  49105  islindeps2  49114  lindssnlvec  49117  fdivmptf  49172  refdivmptf  49173  rrx2linest  49373  itsclc0yqsollem1  49393  itsclc0b  49403  itsclquadb  49407  itscnhlinecirc02plem3  49415  diag1  49933  setc1onsubc  50231