Theorem simpl1 1188

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

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

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

This theorem is referenced by:  simpl11  1245  simpl21  1248  simpl31  1251  simp1l1  1263  simp2l1  1269  simp3l1  1275  3anandirs  1469  rspc3ev  3585  2nreu  4349  f1prex  7018  cocan1  7025  weniso  7086  smogt  7987  smorndom  7988  omeulem1  8191  nnmord  8241  nnmword  8242  difsnen  8582  enfixsn  8609  mapunen  8670  ac6sfi  8746  fipreima  8814  elfiun  8878  ordiso2  8963  wemaplem2  8995  wemapso  8999  en2eqpr  9418  indcardi  9452  fodomfi2  9471  iunfictbso  9525  infmap2  9629  cofsmo  9680  cfsmolem  9681  coftr  9684  fin23lem11  9728  fincssdom  9734  fin23lem26  9736  isf32lem9  9772  ac6num  9890  gchdomtri  10040  gchpwdom  10081  winainflem  10104  tskuni  10194  gruima  10213  gruf  10222  grudomon  10228  elnpi  10399  distrlem4pr  10437  prlem934  10444  addcan  10813  addcan2  10814  divmulass  11310  divmulasscom  11311  ltmul1a  11478  suprleub  11594  supmul1  11597  suprzcl  12050  uzsupss  12328  xleadd1a  12634  xlesubadd  12644  xmulasslem3  12667  xlemul2a  12670  xadddilem  12675  xadddi2  12678  ixxun  12742  icoshftf1o  12852  ioounsn  12855  snunioc  12858  lincmb01cmp  12873  iccf1o  12874  nn0p1elfzo  13075  fzofzim  13079  ltexp2a  13526  leexp2  13531  ltexp2r  13533  exple1  13536  expnlbnd2  13591  fun2dmnop0  13848  ccatass  13933  ccat2s1fvwOLD  13990  swrdswrdlem  14057  ccatopth  14069  repswpfx  14138  2cshw  14166  cshimadifsn  14182  cshimadifsn0  14183  cshco  14189  repsco  14193  s2f1o  14269  limsupgre  14830  addcn2  14942  mulcn2  14944  ntrivcvgmul  15250  binomrisefac  15388  dvdsmodexp  15607  dvdsadd2b  15648  dvdsmod  15670  oexpneg  15686  sadass  15810  gcdass  15885  rplpwr  15897  rppwr  15898  lcmfunsnlem1  15971  coprmdvds2  15988  rpmulgcd2  15990  qredeq  15991  rpdvds  15994  cncongr2  16002  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  odzdvds  16122  modprmn0modprm0  16134  coprimeprodsq2  16136  pythagtriplem3  16145  pcdvdsb  16195  pcgcd1  16203  qexpz  16227  pockthg  16232  vdwnnlem1  16321  0ram  16346  ramz2  16350  lubss  17723  lubun  17725  clatleglb  17728  clatglbss  17729  mrelatglb  17786  isnsgrp  17897  issubmnd  17930  ress0g  17931  gsumccatOLD  17997  gsumccat  17998  frmdss2  18020  submefmnd  18052  mulgneg  18238  mulgdirlem  18250  submmulg  18263  subgmulg  18285  nmzsubg  18309  ghmmulg  18362  gsmsymgreqlem1  18550  pmtrfb  18585  psgnunilem4  18617  odmodnn0  18660  odnncl  18665  odmod  18666  odmulgid  18673  odmulgeq  18676  odf1o1  18689  odf1o2  18690  odngen  18694  gexdvdsi  18700  pgpfi1  18712  odcau  18721  subgslw  18733  fislw  18742  lsmssv  18760  lsmless1x  18761  lsmless2x  18762  lsmsubm  18770  lsmmod  18793  lsmmod2  18794  efgred  18866  cntzcmn  18953  ghmplusg  18959  odadd1  18961  odadd2  18962  odadd  18963  lsmcomx  18969  gsumconst  19047  ablsimpgprmd  19230  srg1zr  19272  ring1eq0  19336  mulgass2  19347  isabvd  19584  rmodislmodlem  19694  rmodislmod  19695  lssintcl  19729  0lmhm  19805  lmhmvsca  19810  reslmhm2b  19819  pwssplit1  19824  pwssplit3  19826  lspfixed  19893  lspsnat  19910  lidldvgen  20021  xrsdsreclblem  20137  regsumsupp  20311  obselocv  20417  uvcresum  20482  frlmsslsp  20485  frlmup4  20490  lindff1  20509  f1lindf  20511  lsslindf  20519  islindf4  20527  lbslcic  20530  issubassa  20555  evlsval2  20759  psrplusgpropd  20865  coe1subfv  20895  coe1mul2  20898  mhmvlin  21004  mpomatmul  21051  mamutpos  21063  scmatscmide  21112  mavmulsolcl  21156  marrepcl  21169  mdetdiag  21204  mdetunilem1  21217  mdetunilem3  21219  mdetunilem7  21223  mdetunilem9  21225  mdetmul  21228  slesolinvbi  21286  m2pmfzmap  21352  pmatcollpwlem  21385  pmatcollpw  21386  mp2pm2mplem4  21414  chpdmatlem3  21445  chfacfisfcpmat  21460  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  chfacfpmmulgsum2  21470  cayhamlem1  21471  cpmidpmatlem2  21476  cpmadugsumlemB  21479  cpmadugsumlemC  21480  cpmadugsumlemF  21481  riinopn  21513  neiint  21709  topssnei  21729  restntr  21787  iscnp4  21868  cnconst2  21888  cnrest2  21891  cnprest2  21895  cnpdis  21898  cnt0  21951  cnt1  21955  cnhaus  21959  ordthauslem  21988  cncmp  21997  fiuncmp  22009  sscmp  22010  hauscmp  22012  cnconn  22027  unconn  22034  nlly2i  22081  llynlly  22082  nllyidm  22094  finlocfin  22125  ptrescn  22244  xkococnlem  22264  qtopss  22320  kqfvima  22335  r0cld  22343  ordthmeolem  22406  fbssint  22443  fmf  22550  fmss  22551  elfm  22552  rnelfmlem  22557  rnelfm  22558  fmco  22566  flimss2  22577  flimss1  22578  flimrest  22588  flftg  22601  cnpflf2  22605  cnpflf  22606  flfcnp  22609  supnfcls  22625  fclsss1  22627  fclsss2  22628  fcfnei  22640  fcfelbas  22641  cnpfcfi  22645  subgntr  22712  opnsubg  22713  cldsubg  22716  ghmcnp  22720  utop2nei  22856  neipcfilu  22902  bldisj  23005  blgt0  23006  bl2in  23007  blss2ps  23010  blss2  23011  blssps  23031  blss  23032  xmetresbl  23044  lpbl  23110  blcld  23112  stdbdbl  23124  metcnp3  23147  metcnp2  23149  txmetcnp  23154  blval2  23169  nmoix  23335  nmoeq0  23342  icoopnst  23544  iocopnst  23545  xrhmeo  23551  nmhmcn  23725  cphsqrtcl2  23791  cphsqrtcl3  23792  cfil3i  23873  caublcls  23913  bcthlem5  23932  cmetcusp1  23957  cssbn  23979  rrxcph  23996  pjth  24043  ovoliunlem2  24107  volun  24149  volsup2  24209  mbfimaopn2  24261  iblconst  24421  itgconst  24422  dvcnp2  24523  dvcn  24524  deg1mul3le  24717  deg1tmle  24718  dvdsq1p  24761  ig1peu  24772  ig1pdvds  24777  coeid3  24837  dgrmulc  24868  efcvx  25044  tanord  25130  logdivlti  25211  logccv  25254  recxpcl  25266  cxpeq  25346  ang180  25400  isosctrlem2  25405  cxp2lim  25562  amgm  25576  muval1  25718  dvdssqf  25723  mumullem2  25765  mumul  25766  bcmono  25861  lgsfcl2  25887  lgsdilem  25908  lgsdirprm  25915  lgsdir  25916  lgsdi  25918  lgsne0  25919  padicabv  26214  brbtwn2  26699  colinearalglem1  26700  colinearalg  26704  axcgrtr  26709  axsegconlem8  26718  axsegconlem9  26719  axsegconlem10  26720  axcontlem8  26765  axcontlem10  26767  elntg2  26779  vtxdlfuhgr1v  27269  umgr2wlk  27735  erclwwlksym  27806  clwwlkfo  27835  clwwlkext2edg  27841  erclwwlknsym  27855  clwwlknon1  27882  numclwwlk2lem1  28161  numclwwlk5  28173  frgrregord13  28181  nvmul0or  28433  ipval2lem2  28487  lnomul  28543  shless  29142  shlej1  29143  pjspansn  29360  hoadddi  29586  kbmul  29738  homco2  29760  kbass2  29900  eliccelico  30526  elicoelioo  30527  iocinioc2  30528  iocinif  30530  swrdrn2  30654  xrge0adddir  30726  xrge0npcan  30728  archiabl  30877  ress1r  30911  rhmdvdsr  30942  pidlnz  30991  intlidl  31010  ssmxidl  31050  pstmfval  31249  fmcncfil  31284  zrhnm  31320  qqhnm  31341  measvunilem  31581  volfiniune  31599  dya2iocnrect  31649  sibfinima  31707  probun  31787  probinc  31789  cndprob01  31803  signstfvp  31951  bnj517  32267  bnj594  32294  pconnpi1  32597  cvmsss2  32634  mrsubcv  32870  msubvrs  32920  dvdspw  33095  br6  33106  br4  33107  frpomin  33191  frrlem4  33239  frrlem10  33245  fprlem1  33250  nosep1o  33299  nosepssdm  33303  nolt02olem  33311  nosupres  33320  nosupbnd1lem1  33321  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd1lem6  33326  nosupbnd2  33329  noetalem2  33331  cgrcomim  33563  cgrtriv  33576  cgrextend  33582  segconeq  33584  btwntriv2  33586  btwnintr  33593  btwnexch3  33594  btwnouttr2  33596  trisegint  33602  cgrsub  33619  cgrxfr  33629  btwnxfr  33630  lineext  33650  btwnconn1lem13  33673  btwnconn1lem14  33674  btwnconn3  33677  segcon2  33679  brsegle  33682  brsegle2  33683  segletr  33688  segleantisym  33689  seglelin  33690  outsideofeu  33705  lineunray  33721  lineelsb2  33722  ivthALT  33796  lindsenlbs  35052  areacirc  35150  cocanfo  35156  upixp  35167  ismtyima  35241  rrndstprj2  35269  zerdivemp1x  35385  lsatfixedN  36305  lssat  36312  eqlkr  36395  eqlkr2  36396  lkrlsp  36398  lshpkrlem4  36409  opposet  36477  cvrcon3b  36573  cvrcmp  36579  atlen0  36606  atnle  36613  atlatmstc  36615  cvlatexch3  36634  cvlsupr2  36639  hlsupr2  36683  hlrelat2  36699  cvrexchlem  36715  lnnat  36723  atcvrj2b  36728  atle  36732  atexchcvrN  36736  atbtwn  36742  athgt  36752  3dimlem3  36757  3dim1  36763  1cvratlt  36770  1cvrjat  36771  ps-1  36773  ps-2  36774  3atlem3  36781  3atlem5  36783  3atlem7  36785  llni  36804  llni2  36808  atcvrlln2  36815  llnexatN  36817  llncmp  36818  2llnmat  36820  2at0mat0  36821  lplni  36828  lplnnle2at  36837  2atnelpln  36840  lplnllnneN  36852  llncvrlpln2  36853  2lplnmN  36855  2llnmj  36856  lplncmp  36858  lplnexatN  36859  lplnexllnN  36860  2llnm3N  36865  lvoli  36871  lvoli3  36873  islvol2aN  36888  4atlem0a  36889  4atlem3  36892  4atlem3a  36893  4atlem4a  36895  4atlem4b  36896  4atlem4c  36897  4atlem4d  36898  4atlem10b  36901  4atlem11  36905  4atlem12  36908  lplncvrlvol2  36911  lvolcmp  36913  2lplnmj  36918  islinei  37036  pmapglbx  37065  linepmap  37071  lneq2at  37074  lnjatN  37076  lncvrat  37078  lncmp  37079  2llnma3r  37084  elpaddatriN  37099  elpaddat  37100  paddcom  37109  paddss1  37113  paddss2  37114  paddss12  37115  paddasslem6  37121  paddasslem7  37122  paddasslem8  37123  paddasslem9  37124  paddasslem15  37130  pmodlem2  37143  pmodl42N  37147  pmapjoin  37148  llnmod1i2  37156  2polcon4bN  37214  polcon2bN  37216  poml4N  37249  poml6N  37251  osumcllem1N  37252  osumcllem2N  37253  osumcllem11N  37262  osumclN  37263  pmapojoinN  37264  pexmidlem2N  37267  pexmidlem3N  37268  pexmidlem4N  37269  pexmidlem6N  37271  pexmidlem7N  37272  pl42lem2N  37276  pl42lem3N  37277  pl42lem4N  37278  pl42N  37279  lhpexle2lem  37305  lhpexle3lem  37307  lhpexle3  37308  lhpmcvr3  37321  lhp2at0nle  37331  lhprelat3N  37336  4atex  37372  4atex2  37373  lauteq  37391  lautco  37393  ltrncoidN  37424  ltrneq2  37444  ltrnnidn  37470  ltrnideq  37471  trlnid  37475  ltrnatlw  37479  trlnle  37482  trlval3  37483  trlval4  37484  cdlemc  37493  cdlemd5  37498  cdlemd9  37502  ltrneq3  37504  cdleme0moN  37521  cdleme20  37620  cdleme21j  37632  cdleme21  37633  cdleme27cl  37662  cdlemefrs29bpre0  37692  cdlemefs27cl  37709  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme32d  37740  cdleme32f  37742  cdleme32le  37743  cdleme35h2  37753  cdleme38n  37760  cdleme40m  37763  cdleme41snaw  37772  cdleme42ke  37781  cdleme17d3  37792  cdleme48fvg  37796  cdlemeg46fvcl  37802  cdlemeg46fgN  37830  cdleme48gfv1  37832  cdleme48fgv  37834  cdleme50trn3  37849  trlord  37865  ltrniotavalbN  37880  cdlemb3  37902  cdlemg6c  37916  cdlemg6  37919  cdlemg7N  37922  cdlemg8c  37925  cdlemg8  37927  cdlemg11a  37933  cdlemg11b  37938  cdlemg12e  37943  cdlemg15a  37951  cdlemg15  37952  cdlemg16  37953  cdlemg16z  37955  cdlemg16zz  37956  cdlemg17dN  37959  cdlemg18a  37974  cdlemg20  37981  cdlemg22  37983  cdlemg24  37984  cdlemg37  37985  cdlemg31d  37996  cdlemg29  38001  cdlemg33b  38003  cdlemg33  38007  cdlemg38  38011  cdlemg39  38012  cdlemg40  38013  trlco  38023  trlcone  38024  cdlemg42  38025  cdlemg44b  38028  ltrncom  38034  trljco  38036  tendococl  38068  tendoplcl  38077  tendoplcom  38078  cdlemj2  38118  cdlemj3  38119  tendoid0  38121  tendoconid  38125  tendotr  38126  cdlemk25-3  38200  cdlemk26b-3  38201  cdlemk34  38206  cdlemk36  38209  cdlemk38  38211  cdlemkid4  38230  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk19x  38239  cdlemk53  38253  cdlemk55  38257  cdlemk55u  38262  cdlemk39u  38264  cdlemk19u  38266  cdlemk56  38267  tendoex  38271  cdleml3N  38274  cdleml5N  38276  tendospcanN  38319  cdlemm10N  38414  cdlemn11pre  38506  dihord2pre  38521  dihvalcqpre  38531  dihopelvalcpre  38544  dihord6apre  38552  dihord5b  38555  dihord5apre  38558  dihord  38560  dihmeetlem1N  38586  dihglblem5apreN  38587  dihglblem3N  38591  dihmeetlem2N  38595  dihglbcpreN  38596  dihmeetbN  38599  dihmeetlem4preN  38602  dihmeetlem5  38604  dihmeetlem7N  38606  dihmeetlem10N  38612  dihmeetlem11N  38613  dihmeetlem12N  38614  dihmeetlem13N  38615  dihmeetlem15N  38617  dihmeetlem16N  38618  dihmeetlem17N  38619  dihmeetlem18N  38620  dihmeetlem19N  38621  dihmeetALTN  38623  dih1dimatlem0  38624  dihlspsnssN  38628  dihlspsnat  38629  mapdh8ad  39075  hdmap14lem14  39177  hgmapvvlem3  39221  resubcan2  39526  mzprename  39690  eldioph2lem1  39701  lzunuz  39709  rencldnfi  39762  pellexlem2  39771  infmrgelbi  39819  pellfundglb  39826  pellfund14gap  39828  qirropth  39849  rmxycomplete  39858  congadd  39907  acongeq  39924  jm2.19  39934  jm2.23  39937  jm2.20nn  39938  jm2.27  39949  jm3.1  39961  aomclem6  40003  lnmepi  40029  lmhmfgsplit  40030  lmhmlnmsplit  40031  pwssplit4  40033  hbtlem2  40068  hbtlem5  40072  dgraa0p  40093  proot1hash  40144  iocunico  40161  relexpxpmin  40418  brtrclfv2  40428  ntrclsiso  40770  ntrclskb  40772  ntrclsk3  40773  k0004lem3  40852  grur1cld  40940  ismnu  40969  grumnudlem  40993  suprnmpt  41798  wessf1ornlem  41811  projf1o  41825  snunioo1  42149  iccintsng  42160  lptre2pt  42282  limcleqr  42286  fnlimfvre  42316  limsupgtlem  42419  volioc  42614  iblspltprt  42615  stoweidlem19  42661  stoweidlem20  42662  stoweidlem22  42664  stoweidlem28  42670  stoweidlem34  42676  stoweidlem44  42686  stoweidlem60  42702  wallispilem3  42709  fourierdlem41  42790  fourierdlem42  42791  fourierdlem49  42797  fourierdlem51  42799  fourierdlem54  42802  fourierdlem74  42822  fourierdlem97  42845  caratheodorylem2  43166  ovnsubaddlem2  43210  hspmbllem2  43266  smflimmpt  43441  smflimsupmpt  43460  smfliminfmpt  43463  fzopredsuc  43880  fzoopth  43884  imasetpreimafvbijlemfv  43919  iccpartigtl  43940  lighneal  44129  oexpnegALTV  44195  oexpnegnz  44196  tgblthelfgott  44333  lidldomn1  44545  ofaddmndmap  44745  lincdifsn  44833  lincellss  44835  lincresunit3lem3  44883  islindeps2  44892  lindssnlvec  44895  fdivmptf  44955  refdivmptf  44956  rrx2linest  45156  itsclc0yqsollem1  45176  itsclc0b  45186  itsclquadb  45190  itscnhlinecirc02plem3  45198