Theorem simpl3 1212

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

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

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 1105

This theorem is referenced by:  simpl13  1269  simpl23  1272  simpl33  1275  simp1l3  1287  simp2l3  1293  simp3l3  1299  3anandirs  1501  2nreu  4410  predtrss  6325  frpomin  6343  f1prex  7284  fcofo  7288  soisores  7327  weniso  7354  knatar  7357  ofmpteq  7699  funelss  8045  frrlem10  8293  fprlem1  8298  smocdmdom  8356  nnmord  8619  nnmword  8620  naddasslem1  8682  naddasslem2  8683  difsnen  9048  mapunen  9135  ac6sfi  9245  fipreima  9316  wemaplem2  9510  wemapso2lem  9515  ttrclselem2  9696  en2eqpr  9992  indcardi  10026  acndom  10036  fodomfi2  10045  infmap2  10201  cflim2  10248  coftr  10258  infpssrlem4  10291  fin23lem11  10302  fincssdom  10308  isf32lem9  10346  fin1a2lem9  10393  gchpwdom  10656  gruima  10788  prpssnq  10976  distrlem4pr  11012  dedekind  11374  addcan  11395  addcan2  11396  divmulass  11896  supmul1  12185  uzsupss  12965  xaddass  13276  xleadd1a  13280  xlesubadd  13290  xmulasslem3  13313  xmulass  13314  xadddilem  13321  xadddi  13322  ixxun  13389  icoshftf1o  13502  snunioc  13508  difelfzle  13671  fzo1fzo0n0  13746  ssfzoulel  13791  modmuladd  13951  modifeq2int  13971  modaddmulmod  13976  modsubdir  13978  ltexp2a  14204  leexp2  14209  ltexp2r  14211  exple1  14215  expnlbnd2  14272  mulsubdivbinom2  14300  hashtpg  14524  ccatass  14628  ccatopth  14755  pfxccatin12lem2a  14766  pfxccat3  14773  cshinj  14850  2cshw  14852  s2f1o  14955  limsupgre  15534  addcn2  15647  mulcn2  15649  binomrisefac  16097  bpolydif  16110  dvdsmodexp  16319  modmulconst  16347  dvdsexp2im  16386  dvdsmod  16388  sadass  16530  gcdass  16606  rplpwr  16617  rpmulgcd2  16715  rpdvds  16719  rpexp  16782  prmdiveq  16846  hashgcdlem  16848  coprimeprodsq  16869  coprimeprodsq2  16870  pythagtriplem3  16879  pcdvdsb  16930  pcgcd1  16938  dvdsprmpweq  16945  pcbc  16961  0ram  17081  ramz2  17085  ramub1lem1  17087  mremre  17657  mrieqv2d  17696  lubun  18572  isnsgrp  18782  issubmnd  18820  frmdss2  18923  submefmnd  18955  sgrp2rid2ex  18990  mulgnn0p1  19152  mulgnnsubcl  19153  mulgneg  19159  mulgdirlem  19172  nmzsubg  19232  ghmmulg  19299  pmtrfv  19523  pmtrmvd  19527  pmtrfb  19536  odmodnn0  19611  oddvdsnn0  19615  odnncl  19616  odmod  19617  oddvds  19618  odeq  19621  odmulgid  19625  odmulg  19627  odmulgeq  19628  odbezout  19629  odf1o1  19643  odf1o2  19644  odngen  19648  odcau  19675  pgpssslw  19685  fislw  19696  lsmless1x  19715  lsmless2x  19716  lsmsubm  19724  lsmmod  19746  lsmmod2  19747  efgsfo  19810  cntzcmn  19911  odadd1  19919  odadd2  19920  odadd  19921  lsmcomx  19927  prdscmnd  19932  gsumconst  20005  ring1eq0  20382  cntzsubrng  20653  cntzsubr  20692  isabvd  20896  rmodislmod  21032  lspss  21086  0lmhm  21142  reslmhm2  21155  pwssplit0  21160  pwssplit1  21161  lbspss  21184  lspfixed  21233  lsmcv  21246  lspsnat  21250  pidlnz  21355  2idlcpblrng  21391  cnfldfunALT  21518  xrsdsreclblem  21544  obselocv  21859  frlmsplit2  21904  frlmsslss2  21906  frlmup4  21932  lindff1  21951  lsslindf  21961  lsslinds  21962  islindf4  21969  issubassa  21998  aspss  22007  coe1subfv  22408  coe1tm  22415  mpomatmul  22584  mamutpos  22596  submaval  22719  mdetdiag  22737  mdetunilem1  22750  mdetunilem3  22752  mdetunilem9  22758  mdetmul  22761  maducoeval2  22778  madurid  22782  minmar1val  22786  cramer  22829  cpmatel2  22851  m2cpm  22879  decpmatmul  22910  pmatcollpw1lem2  22913  pmatcollpw1  22914  pmatcollpw2lem  22915  pm2mpcl  22935  mply1topmatcl  22943  mp2pm2mplem2  22945  mp2pm2mplem4  22947  pm2mpghmlem2  22950  pm2mpghmlem1  22951  cayhamlem2  23022  neiint  23242  topssnei  23262  cnrest2  23424  cnprest2  23428  cnt0  23484  cnt1  23488  cnhaus  23492  cncmp  23530  fiuncmp  23542  sscmp  23543  hauscmp  23545  cnconn  23560  unconn  23567  comppfsc  23670  kgen2ss  23693  ptpjopn  23750  ptrescn  23777  qtopss  23853  kqfvima  23868  r0cld  23876  cmphaushmeo  23938  fbssint  23976  fbasrn  24022  filuni  24023  ufilmax  24045  fin1aufil  24070  fmf  24083  fmss  24084  rnelfmlem  24090  rnelfm  24091  fmufil  24097  fmco  24099  flimss2  24110  flimss1  24111  flimrest  24121  cnpflf2  24138  cnpflf  24139  flfcnp  24142  lmflf  24143  supnfcls  24158  fclsss1  24160  fclsss2  24161  cnpfcfi  24178  subgntr  24245  opnsubg  24246  cldsubg  24249  ustuqtop1  24379  ucncn  24422  bldisj  24536  blgt0  24537  bl2in  24538  blss2ps  24541  blss2  24542  xbln0  24552  blssps  24562  blss  24563  lpbl  24641  blcld  24643  blcls  24644  stdbdmopn  24656  metcnp2  24680  txmetcnp  24685  blval2  24700  restmetu  24708  nmoix  24867  nmoi2  24868  nmoeq0  24874  nmotri  24877  metdsge  24988  metds0  24989  metdseq0  24993  icoopnst  25079  iccpnfhmeo  25085  xrhmeo  25086  nmhmcn  25260  cphsqrtcl2  25326  cphsqrtcl3  25327  fmcfil  25412  bcthlem5  25468  cmetcusp1  25493  cssbn  25515  pjth  25579  ovolunnul  25640  volun  25685  voliunlem2  25691  itg2const  25880  iblconst  25958  itgconst  25959  limcvallem  26011  dvcnp2  26060  dvcn  26061  deg1mul3le  26255  deg1tmle  26256  idomrootle  26311  ig1pdvds  26318  coe11  26391  dgrmulc  26409  dvply1  26426  aaliou2  26484  efcvx  26593  tanord  26684  logdivlti  26766  logccv  26809  recxpcl  26821  cxplea  26842  cxple2a  26845  ang180  26960  isosctrlem2  26965  cxp2lim  27122  amgm  27136  muval1  27278  dvdssqf  27283  mumullem2  27325  bcmono  27422  lgsneg  27466  lgsmod  27468  lgsdirprm  27476  lgsdir  27477  lgsdi  27479  ltsres  27807  nolt02olem  27839  nolt02o  27840  nogt01o  27841  nosupbnd1lem1  27853  nosupbnd1lem4  27856  nosupbnd1lem5  27857  nosupbnd1lem6  27858  noinfbnd1lem1  27868  noinfbnd1lem4  27871  noinfbnd1lem6  27873  noinfbnd2  27876  noetainflem3  27884  ltslpss  28082  cofslts  28092  coinitslts  28093  cofcutrtime  28101  addsass  28179  addsdi  28329  mulsass  28340  ltmuls2  28345  norecdiv  28364  z12bdaylem  28658  brbtwn2  29236  colinearalglem1  29237  colinearalg  29241  axcgrtr  29246  axcontlem2  29296  upgrewlkle2  29937  wlksoneq1eq2  29993  crctcshwlkn0lem5  30144  wspthsnwspthsnon  30246  lppthon  30483  upgriseupth  30539  4cyclusnfrgr  30624  numclwwlk1lem2foa  30686  numclwwlk5  30720  nvmul0or  30983  shless  31692  shlej1  31693  pjspansn  31910  kbmul  32288  homco2  32310  kbass2  32450  fnpreimac  32996  padct  33044  eliccelico  33103  elicoelioo  33104  iocinioc2  33105  difioo  33108  nexple  33158  swrdrn2  33255  swrdrn3  33256  xrge0npcan  33321  isarchi2  33486  archiabl  33499  lindssn  33672  ssmxidl  33738  mdetlap1  34197  zarclsiin  34242  pstmfval  34267  fmcncfil  34302  zrhnm  34338  qqhnm  34361  volfiniune  34601  omsmeas  34694  eulerpartlemb  34739  probinc  34792  cndprob01  34806  signswmnd  34925  cvmsss2  35747  funsseq  36241  cgrtriv  36475  5segofs  36479  btwntriv2  36485  btwnxfr  36529  segcon2  36578  brsegle2  36582  seglelin  36589  outsideofeu  36604  nmulss1  36672  ltnmul  36674  nmulle  36675  ltnadd  36676  naddle  36677  weiunpo  36957  weiunfr  36959  weiunse  36960  lindsenlbs  38247  mblfinlem2  38290  blbnd  38419  rrndstprj2  38463  zerdivemp1x  38579  lsmsat  39763  lsatfixedN  39764  lssat  39771  lkrlsp  39857  lshpkrlem4  39868  cvrcon3b  40032  leat3  40050  atlen0  40065  atnle  40072  atlatmstc  40074  atlatle  40075  cvlcvr1  40094  cvlsupr2  40098  hlsupr2  40142  hlrelat2  40158  cvrexchlem  40174  cvratlem  40176  lnnat  40182  atexchcvrN  40195  1cvratlt  40229  1cvrjat  40230  3atlem3  40240  3atlem7  40244  llni2  40267  atcvrlln2  40274  llnexatN  40276  llncmp  40277  2llnmat  40279  2at0mat0  40280  2atnelpln  40299  llncvrlpln2  40312  2lplnmN  40314  2llnmj  40315  lplncmp  40317  lplnexatN  40318  2llnjaN  40321  lvoli3  40332  islvol2aN  40347  4atlem3a  40352  4atlem4a  40354  4atlem4b  40355  4atlem11  40364  4atlem12  40367  lplncvrlvol2  40370  lvolcmp  40372  2lplnmj  40377  islinei  40495  linepmap  40530  lneq2at  40533  2llnma3r  40543  elpaddn0  40555  elpaddatriN  40558  elpaddat  40559  paddcom  40568  paddss1  40572  paddss2  40573  paddasslem6  40580  paddasslem7  40581  paddasslem10  40584  paddasslem15  40589  pmodlem2  40602  pmodl42N  40606  pmapjoin  40607  atmod1i1m  40613  llnmod1i2  40615  llnexchb2lem  40623  polcon2bN  40675  pclfinclN  40705  poml4N  40708  poml6N  40710  osumcllem11N  40721  osumclN  40722  pmapojoinN  40723  pexmidlem2N  40726  pexmidlem3N  40727  pexmidlem4N  40728  pexmidlem6N  40730  pexmidlem7N  40731  pl42lem2N  40735  pl42lem3N  40736  pl42lem4N  40737  pl42N  40738  lhpexle3lem  40766  lhpmcvr3  40780  lhp2at0nle  40790  lhprelat3N  40795  lauteq  40850  lautco  40852  ltrncoidN  40883  ltrneq2  40903  ltrnnidn  40929  ltrnideq  40930  trlnle  40941  cdlemc  40952  cdlemd4  40956  cdlemd5  40957  cdlemd9  40961  cdlemd  40962  ltrneq3  40963  cdlemefrs29pre00  41150  cdlemefrs29cpre1  41153  cdlemefrs29clN  41154  cdlemefrs32fva  41155  cdlemefr29exN  41157  cdlemefr27cl  41158  cdlemefs27cl  41168  cdlemefs32sn1aw  41169  cdleme32fva  41192  cdleme32d  41199  cdleme32f  41201  cdleme32le  41202  cdleme40n  41223  cdleme41snaw  41231  cdleme17d3  41251  cdleme48fvg  41255  cdlemeg46fvcl  41261  cdlemeg46fgN  41289  cdleme48fgv  41293  ltrniotavalbN  41339  cdlemb3  41361  cdlemg15  41411  cdlemg17dN  41418  trlco  41482  cdlemg44b  41487  ltrncom  41493  trljco  41495  tendococl  41527  tendoplcl  41536  tendoplcom  41537  tendotr  41585  cdlemk36  41668  cdlemk35s-id  41693  cdlemk39s-id  41695  cdlemk19x  41698  cdlemk53b  41711  cdlemk55  41716  cdlemk35u  41719  cdlemk55u  41721  cdlemk39u  41723  cdlemk19u  41725  cdlemk56  41726  tendoex  41730  cdleml5N  41735  dihord2pre  41980  dihord6apre  42011  dihord5b  42014  dihord5apre  42017  dihord  42019  dihmeetlem1N  42045  dihmeetlem2N  42054  dihglbcpreN  42055  dihmeetbN  42058  dihmeetlem4preN  42061  dihmeetlem5  42063  dihmeetlem6  42064  dihmeetlem7N  42065  dihmeetlem10N  42071  dihmeetlem11N  42072  dihmeetlem12N  42073  dihmeetlem13N  42074  dihmeetlem15N  42076  dihmeetlem17N  42078  dihmeetlem18N  42079  dihmeetlem19N  42080  dihmeetALTN  42082  dih1dimatlem0  42083  dihlspsnssN  42087  dvh3dim2  42203  sticksstones1  42894  sticksstones2  42895  sticksstones12  42906  aks6d1c6isolem1  42922  dvdsexpnn  43075  resubcan2  43130  mzpsubst  43462  diophrw  43473  eldioph2lem1  43474  rencldnfi  43531  pellexlem2  43540  pellqrexplicit  43587  infmrgelbi  43588  rmxycomplete  43627  congadd  43676  acongeq  43693  jm2.19  43703  jm2.22  43705  jm2.20nn  43707  jm2.25lem1  43708  jm2.27  43718  jm3.1  43730  lmhmlnmsplit  43797  pwssplit4  43799  hbtlem2  43834  dgraa0p  43859  proot1hash  43905  iocunico  43921  cantnf2  44035  dflim5  44039  omcl2  44043  tfsconcatrn  44052  nadd2rabex  44096  relexpxpmin  44426  brtrclfv2  44436  ntrclsk3  44779  grur1cld  44939  ismnu  44954  suprnmpt  45875  wessf1ornlem  45886  choicefi  45900  supxrgere  46032  supxrgelem  46036  supxrge  46037  infleinflem2  46069  snunioo1  46211  iccintsng  46222  fmul01  46279  lptre2pt  46337  0ellimcdiv  46346  fnlimfvre  46371  limsupmnfuzlem  46423  climisp  46443  limsupgtlem  46474  ibliccsinexp  46648  iblioosinexp  46650  volioc  46669  iblspltprt  46670  stoweidlem20  46717  stoweidlem22  46719  stoweidlem34  46731  stoweidlem44  46741  stoweidlem60  46757  wallispilem3  46764  fourierdlem42  46846  fourierdlem51  46854  fourierdlem54  46857  fourierdlem87  46890  fourierdlem97  46900  ioorrnopnlem  47001  sge0seq  47143  hoicvr  47245  fsupdm  47539  finfdm  47543  3f1oss1  47795  funfocofob  47798  imasetpreimafvbijlemfv  48134  uhgrimisgrgric  48679  uhgrimgrlim  48735  fprmappr  49108  lincresunit3lem3  49237  lindssnlvec  49249  rrx2linesl  49506  line2  49515  itsclc0lem3  49521  itsclc0yqsollem1  49525  itscnhlc0xyqsol  49528  itschlc0xyqsol1  49529  itsclc0  49534  itscnhlinecirc02plem2  49546  itscnhlinecirc02plem3  49547  uptrlem1  49971  uptr2  49982  setc1onsubc  50363