Theorem simpl3 1195

Description: Simplification of conjunction. (Contributed by Jeff Hankins, 17-Nov-2009.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl3	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Proof of Theorem simpl3

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2antl3 1189	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:  simpl13  1252  simpl23  1255  simpl33  1258  simp1l3  1270  simp2l3  1276  simp3l3  1282  3anandirs  1475  2nreu  4384  predtrss  6286  frpomin  6304  f1prex  7239  fcofo  7243  soisores  7282  weniso  7309  knatar  7312  ofmpteq  7654  funelss  8000  frrlem10  8245  fprlem1  8250  smocdmdom  8308  nnmord  8568  nnmword  8569  naddasslem1  8630  naddasslem2  8631  difsnen  8997  mapunen  9084  ac6sfi  9194  fipreima  9268  wemaplem2  9462  wemapso2lem  9467  ttrclselem2  9647  en2eqpr  9929  indcardi  9963  acndom  9973  fodomfi2  9982  infmap2  10139  cflim2  10185  coftr  10195  infpssrlem4  10228  fin23lem11  10239  fincssdom  10245  isf32lem9  10283  fin1a2lem9  10330  gchpwdom  10593  gruima  10725  prpssnq  10913  distrlem4pr  10949  dedekind  11309  addcan  11330  addcan2  11331  divmulass  11832  supmul1  12125  uzsupss  12890  xaddass  13201  xleadd1a  13205  xlesubadd  13215  xmulasslem3  13238  xmulass  13239  xadddilem  13246  xadddi  13247  ixxun  13314  icoshftf1o  13427  snunioc  13433  difelfzle  13595  fzo1fzo0n0  13670  ssfzoulel  13715  modmuladd  13875  modifeq2int  13895  modaddmulmod  13900  modsubdir  13902  ltexp2a  14128  leexp2  14133  ltexp2r  14135  exple1  14139  expnlbnd2  14196  mulsubdivbinom2  14224  hashtpg  14447  ccatass  14551  ccatopth  14678  pfxccatin12lem2a  14689  pfxccat3  14696  cshinj  14773  2cshw  14775  s2f1o  14878  limsupgre  15443  addcn2  15556  mulcn2  15558  binomrisefac  16007  bpolydif  16020  dvdsmodexp  16229  modmulconst  16257  dvdsexp2im  16296  dvdsmod  16298  sadass  16440  gcdass  16516  rplpwr  16527  rpmulgcd2  16625  rpdvds  16629  rpexp  16692  prmdiveq  16756  hashgcdlem  16758  coprimeprodsq  16779  coprimeprodsq2  16780  pythagtriplem3  16789  pcdvdsb  16840  pcgcd1  16848  dvdsprmpweq  16855  pcbc  16871  0ram  16991  ramz2  16995  ramub1lem1  16997  mremre  17566  mrieqv2d  17605  lubun  18481  isnsgrp  18691  issubmnd  18729  frmdss2  18831  submefmnd  18863  sgrp2rid2ex  18898  mulgnn0p1  19061  mulgnnsubcl  19062  mulgneg  19068  mulgdirlem  19081  nmzsubg  19140  ghmmulg  19203  pmtrfv  19427  pmtrmvd  19431  pmtrfb  19440  odmodnn0  19515  oddvdsnn0  19519  odnncl  19520  odmod  19521  oddvds  19522  odeq  19525  odmulgid  19529  odmulg  19531  odmulgeq  19532  odbezout  19533  odf1o1  19547  odf1o2  19548  odngen  19552  odcau  19579  pgpssslw  19589  fislw  19600  lsmless1x  19619  lsmless2x  19620  lsmsubm  19628  lsmmod  19650  lsmmod2  19651  efgsfo  19714  cntzcmn  19815  odadd1  19823  odadd2  19824  odadd  19825  lsmcomx  19831  prdscmnd  19836  gsumconst  19909  ring1eq0  20279  cntzsubrng  20544  cntzsubr  20583  isabvd  20789  rmodislmod  20925  lspss  20979  0lmhm  21035  reslmhm2  21048  pwssplit0  21053  pwssplit1  21054  lbspss  21077  lspfixed  21126  lsmcv  21139  lspsnat  21143  2idlcpblrng  21269  cnfldfunALT  21367  xrsdsreclblem  21393  obselocv  21708  frlmsplit2  21753  frlmsslss2  21755  frlmup4  21781  lindff1  21800  lsslindf  21810  lsslinds  21811  islindf4  21818  issubassa  21847  aspss  21856  coe1subfv  22231  coe1tm  22238  mpomatmul  22411  mamutpos  22423  submaval  22546  mdetdiag  22564  mdetunilem1  22577  mdetunilem3  22579  mdetunilem9  22585  mdetmul  22588  maducoeval2  22605  madurid  22609  minmar1val  22613  cramer  22656  cpmatel2  22678  m2cpm  22706  decpmatmul  22737  pmatcollpw1lem2  22740  pmatcollpw1  22741  pmatcollpw2lem  22742  pm2mpcl  22762  mply1topmatcl  22770  mp2pm2mplem2  22772  mp2pm2mplem4  22774  pm2mpghmlem2  22777  pm2mpghmlem1  22778  cayhamlem2  22849  neiint  23069  topssnei  23089  cnrest2  23251  cnprest2  23255  cnt0  23311  cnt1  23315  cnhaus  23319  cncmp  23357  fiuncmp  23369  sscmp  23370  hauscmp  23372  cnconn  23387  unconn  23394  comppfsc  23497  kgen2ss  23520  ptpjopn  23577  ptrescn  23604  qtopss  23680  kqfvima  23695  r0cld  23703  cmphaushmeo  23765  fbssint  23803  fbasrn  23849  filuni  23850  ufilmax  23872  fin1aufil  23897  fmf  23910  fmss  23911  rnelfmlem  23917  rnelfm  23918  fmufil  23924  fmco  23926  flimss2  23937  flimss1  23938  flimrest  23948  cnpflf2  23965  cnpflf  23966  flfcnp  23969  lmflf  23970  supnfcls  23985  fclsss1  23987  fclsss2  23988  cnpfcfi  24005  subgntr  24072  opnsubg  24073  cldsubg  24076  ustuqtop1  24206  ucncn  24249  bldisj  24363  blgt0  24364  bl2in  24365  blss2ps  24368  blss2  24369  xbln0  24379  blssps  24389  blss  24390  lpbl  24468  blcld  24470  blcls  24471  stdbdmopn  24483  metcnp2  24507  txmetcnp  24512  blval2  24527  restmetu  24535  nmoix  24694  nmoi2  24695  nmoeq0  24701  nmotri  24704  metdsge  24815  metds0  24816  metdseq0  24820  icoopnst  24906  iccpnfhmeo  24912  xrhmeo  24913  nmhmcn  25087  cphsqrtcl2  25153  cphsqrtcl3  25154  fmcfil  25239  bcthlem5  25295  cmetcusp1  25320  cssbn  25342  pjth  25406  ovolunnul  25467  volun  25512  voliunlem2  25518  itg2const  25707  iblconst  25785  itgconst  25786  limcvallem  25838  dvcnp2  25887  dvcn  25888  deg1mul3le  26082  deg1tmle  26083  idomrootle  26138  ig1pdvds  26145  coe11  26218  dgrmulc  26236  dvply1  26250  aaliou2  26306  efcvx  26414  tanord  26502  logdivlti  26584  logccv  26627  recxpcl  26639  cxplea  26660  cxple2a  26663  ang180  26778  isosctrlem2  26783  cxp2lim  26940  amgm  26954  muval1  27096  dvdssqf  27101  mumullem2  27143  bcmono  27240  lgsneg  27284  lgsmod  27286  lgsdirprm  27294  lgsdir  27295  lgsdi  27297  ltsres  27626  nolt02olem  27658  nolt02o  27659  nogt01o  27660  nosupbnd1lem1  27672  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  noinfbnd1lem1  27687  noinfbnd1lem4  27690  noinfbnd1lem6  27692  noinfbnd2  27695  noetainflem3  27703  ltslpss  27900  cofslts  27910  coinitslts  27911  cofcutrtime  27919  addsass  27997  addsdi  28147  mulsass  28158  ltmuls2  28163  norecdiv  28182  z12bdaylem  28476  brbtwn2  28974  colinearalglem1  28975  colinearalg  28979  axcgrtr  28984  axcontlem2  29034  upgrewlkle2  29675  wlksoneq1eq2  29731  crctcshwlkn0lem5  29882  wspthsnwspthsnon  29984  lppthon  30221  upgriseupth  30277  4cyclusnfrgr  30362  numclwwlk1lem2foa  30424  numclwwlk5  30458  nvmul0or  30721  shless  31430  shlej1  31431  pjspansn  31648  kbmul  32026  homco2  32048  kbass2  32188  fnpreimac  32743  padct  32791  eliccelico  32850  elicoelioo  32851  iocinioc2  32852  difioo  32855  nexple  32917  swrdrn2  33014  swrdrn3  33015  xrge0npcan  33080  isarchi2  33246  archiabl  33259  pidlnz  33436  lindssn  33438  ssmxidl  33534  mdetlap1  33970  zarclsiin  34015  pstmfval  34040  fmcncfil  34075  zrhnm  34111  qqhnm  34134  volfiniune  34374  omsmeas  34467  eulerpartlemb  34512  probinc  34565  cndprob01  34579  signswmnd  34701  cvmsss2  35456  funsseq  35950  cgrtriv  36184  5segofs  36188  btwntriv2  36194  btwnxfr  36238  segcon2  36287  brsegle2  36291  seglelin  36298  outsideofeu  36313  weiunpo  36647  weiunfr  36649  weiunse  36650  lindsenlbs  37936  mblfinlem2  37979  blbnd  38108  rrndstprj2  38152  zerdivemp1x  38268  lsmsat  39454  lsatfixedN  39455  lssat  39462  lkrlsp  39548  lshpkrlem4  39559  cvrcon3b  39723  leat3  39741  atlen0  39756  atnle  39763  atlatmstc  39765  atlatle  39766  cvlcvr1  39785  cvlsupr2  39789  hlsupr2  39833  hlrelat2  39849  cvrexchlem  39865  cvratlem  39867  lnnat  39873  atexchcvrN  39886  1cvratlt  39920  1cvrjat  39921  3atlem3  39931  3atlem7  39935  llni2  39958  atcvrlln2  39965  llnexatN  39967  llncmp  39968  2llnmat  39970  2at0mat0  39971  2atnelpln  39990  llncvrlpln2  40003  2lplnmN  40005  2llnmj  40006  lplncmp  40008  lplnexatN  40009  2llnjaN  40012  lvoli3  40023  islvol2aN  40038  4atlem3a  40043  4atlem4a  40045  4atlem4b  40046  4atlem11  40055  4atlem12  40058  lplncvrlvol2  40061  lvolcmp  40063  2lplnmj  40068  islinei  40186  linepmap  40221  lneq2at  40224  2llnma3r  40234  elpaddn0  40246  elpaddatriN  40249  elpaddat  40250  paddcom  40259  paddss1  40263  paddss2  40264  paddasslem6  40271  paddasslem7  40272  paddasslem10  40275  paddasslem15  40280  pmodlem2  40293  pmodl42N  40297  pmapjoin  40298  atmod1i1m  40304  llnmod1i2  40306  llnexchb2lem  40314  polcon2bN  40366  pclfinclN  40396  poml4N  40399  poml6N  40401  osumcllem11N  40412  osumclN  40413  pmapojoinN  40414  pexmidlem2N  40417  pexmidlem3N  40418  pexmidlem4N  40419  pexmidlem6N  40421  pexmidlem7N  40422  pl42lem2N  40426  pl42lem3N  40427  pl42lem4N  40428  pl42N  40429  lhpexle3lem  40457  lhpmcvr3  40471  lhp2at0nle  40481  lhprelat3N  40486  lauteq  40541  lautco  40543  ltrncoidN  40574  ltrneq2  40594  ltrnnidn  40620  ltrnideq  40621  trlnle  40632  cdlemc  40643  cdlemd4  40647  cdlemd5  40648  cdlemd9  40652  cdlemd  40653  ltrneq3  40654  cdlemefrs29pre00  40841  cdlemefrs29cpre1  40844  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdlemefr29exN  40848  cdlemefr27cl  40849  cdlemefs27cl  40859  cdlemefs32sn1aw  40860  cdleme32fva  40883  cdleme32d  40890  cdleme32f  40892  cdleme32le  40893  cdleme40n  40914  cdleme41snaw  40922  cdleme17d3  40942  cdleme48fvg  40946  cdlemeg46fvcl  40952  cdlemeg46fgN  40980  cdleme48fgv  40984  ltrniotavalbN  41030  cdlemb3  41052  cdlemg15  41102  cdlemg17dN  41109  trlco  41173  cdlemg44b  41178  ltrncom  41184  trljco  41186  tendococl  41218  tendoplcl  41227  tendoplcom  41228  tendotr  41276  cdlemk36  41359  cdlemk35s-id  41384  cdlemk39s-id  41386  cdlemk19x  41389  cdlemk53b  41402  cdlemk55  41407  cdlemk35u  41410  cdlemk55u  41412  cdlemk39u  41414  cdlemk19u  41416  cdlemk56  41417  tendoex  41421  cdleml5N  41426  dihord2pre  41671  dihord6apre  41702  dihord5b  41705  dihord5apre  41708  dihord  41710  dihmeetlem1N  41736  dihmeetlem2N  41745  dihglbcpreN  41746  dihmeetbN  41749  dihmeetlem4preN  41752  dihmeetlem5  41754  dihmeetlem6  41755  dihmeetlem7N  41756  dihmeetlem10N  41762  dihmeetlem11N  41763  dihmeetlem12N  41764  dihmeetlem13N  41765  dihmeetlem15N  41767  dihmeetlem17N  41769  dihmeetlem18N  41770  dihmeetlem19N  41771  dihmeetALTN  41773  dih1dimatlem0  41774  dihlspsnssN  41778  dvh3dim2  41894  sticksstones1  42585  sticksstones2  42586  sticksstones12  42597  aks6d1c6isolem1  42613  dvdsexpnn  42765  resubcan2  42820  mzpsubst  43180  diophrw  43191  eldioph2lem1  43192  rencldnfi  43249  pellexlem2  43258  pellqrexplicit  43305  infmrgelbi  43306  rmxycomplete  43345  congadd  43394  acongeq  43411  jm2.19  43421  jm2.22  43423  jm2.20nn  43425  jm2.25lem1  43426  jm2.27  43436  jm3.1  43448  lmhmlnmsplit  43515  pwssplit4  43517  hbtlem2  43552  dgraa0p  43577  proot1hash  43623  iocunico  43639  cantnf2  43753  dflim5  43757  omcl2  43761  tfsconcatrn  43770  nadd2rabex  43814  relexpxpmin  44144  brtrclfv2  44154  ntrclsk3  44497  grur1cld  44659  ismnu  44688  suprnmpt  45604  wessf1ornlem  45615  choicefi  45629  supxrgere  45763  supxrgelem  45767  supxrge  45768  infleinflem2  45800  snunioo1  45942  iccintsng  45953  fmul01  46010  lptre2pt  46068  0ellimcdiv  46077  fnlimfvre  46102  limsupmnfuzlem  46154  climisp  46174  limsupgtlem  46205  ibliccsinexp  46379  iblioosinexp  46381  volioc  46400  iblspltprt  46401  stoweidlem20  46448  stoweidlem22  46450  stoweidlem34  46462  stoweidlem44  46472  stoweidlem60  46488  wallispilem3  46495  fourierdlem42  46577  fourierdlem51  46585  fourierdlem54  46588  fourierdlem87  46621  fourierdlem97  46631  ioorrnopnlem  46732  sge0seq  46874  hoicvr  46976  fsupdm  47270  finfdm  47274  3f1oss1  47523  funfocofob  47526  imasetpreimafvbijlemfv  47862  uhgrimisgrgric  48407  uhgrimgrlim  48463  fprmappr  48821  lincresunit3lem3  48950  lindssnlvec  48962  rrx2linesl  49219  line2  49228  itsclc0lem3  49234  itsclc0yqsollem1  49238  itscnhlc0xyqsol  49241  itschlc0xyqsol1  49242  itsclc0  49247  itscnhlinecirc02plem2  49259  itscnhlinecirc02plem3  49260  uptrlem1  49685  uptr2  49696  setc1onsubc  50077