Theorem simpl3 1192

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  simpl13  1249  simpl23  1252  simpl33  1255  simp1l3  1267  simp2l3  1273  simp3l3  1279  3anandirs  1471  2nreu  4376  predtrss  6229  frpomin  6247  f1prex  7165  fcofo  7169  soisores  7207  weniso  7234  knatar  7237  ofmpteq  7564  funelss  7897  frrlem10  8120  fprlem1  8125  smorndom  8208  nnmord  8472  nnmword  8473  difsnen  8849  mapunen  8942  ac6sfi  9067  fipreima  9134  wemaplem2  9315  wemapso2lem  9320  ttrclselem2  9493  en2eqpr  9772  indcardi  9806  acndom  9816  fodomfi2  9825  infmap2  9983  cflim2  10028  coftr  10038  infpssrlem4  10071  fin23lem11  10082  fincssdom  10088  isf32lem9  10126  fin1a2lem9  10173  gchpwdom  10435  gruima  10567  prpssnq  10755  distrlem4pr  10791  dedekind  11147  addcan  11168  addcan2  11169  divmulass  11665  supmul1  11953  uzsupss  12689  xaddass  12992  xleadd1a  12996  xlesubadd  13006  xmulasslem3  13029  xmulass  13030  xadddilem  13037  xadddi  13038  ixxun  13104  icoshftf1o  13215  snunioc  13221  difelfzle  13378  fzo1fzo0n0  13447  ssfzoulel  13490  modmuladd  13642  modifeq2int  13662  modaddmulmod  13667  modsubdir  13669  ltexp2a  13893  leexp2  13898  ltexp2r  13900  exple1  13903  expnlbnd2  13958  mulsubdivbinom2  13985  hashtpg  14208  ccatass  14302  ccatopth  14438  pfxccatin12lem2a  14449  pfxccat3  14456  cshinj  14533  2cshw  14535  s2f1o  14638  limsupgre  15199  addcn2  15312  mulcn2  15314  binomrisefac  15761  bpolydif  15774  dvdsmodexp  15980  modmulconst  16006  dvdsexp2im  16045  dvdsmod  16047  sadass  16187  gcdass  16264  rplpwr  16276  rpmulgcd2  16370  rpdvds  16374  rpexp  16436  prmdiveq  16496  hashgcdlem  16498  coprimeprodsq  16518  coprimeprodsq2  16519  pythagtriplem3  16528  pcdvdsb  16579  pcgcd1  16587  dvdsprmpweq  16594  pcbc  16610  0ram  16730  ramz2  16734  ramub1lem1  16736  mremre  17322  mrieqv2d  17357  lubun  18242  isnsgrp  18388  issubmnd  18421  gsumccatOLD  18488  frmdss2  18511  submefmnd  18543  sgrp2rid2ex  18575  mulgnn0p1  18724  mulgnnsubcl  18725  mulgneg  18731  mulgdirlem  18743  nmzsubg  18802  ghmmulg  18855  pmtrfv  19069  pmtrmvd  19073  pmtrfb  19082  odmodnn0  19157  oddvdsnn0  19161  odnncl  19162  odmod  19163  oddvds  19164  odeq  19167  odmulgid  19170  odmulg  19172  odmulgeq  19173  odbezout  19174  odf1o1  19186  odf1o2  19187  odngen  19191  odcau  19218  pgpssslw  19228  fislw  19239  lsmless1x  19258  lsmless2x  19259  lsmsubm  19267  lsmmod  19290  lsmmod2  19291  efgsfo  19354  cntzcmn  19450  odadd1  19458  odadd2  19459  odadd  19460  lsmcomx  19466  prdscmnd  19471  gsumconst  19544  ring1eq0  19838  cntzsubr  20066  isabvd  20089  rmodislmod  20200  rmodislmodOLD  20201  lspss  20255  0lmhm  20311  reslmhm2  20324  pwssplit0  20329  pwssplit1  20330  lbspss  20353  lspfixed  20399  lsmcv  20412  lspsnat  20416  cnfldfunALT  20619  xrsdsreclblem  20653  obselocv  20944  frlmsplit2  20989  frlmsslss2  20991  frlmup4  21017  lindff1  21036  lsslindf  21046  lsslinds  21047  islindf4  21054  issubassa  21082  aspss  21090  coe1subfv  21446  coe1tm  21453  mpomatmul  21604  mamutpos  21616  submaval  21739  mdetdiag  21757  mdetunilem1  21770  mdetunilem3  21772  mdetunilem9  21778  mdetmul  21781  maducoeval2  21798  madurid  21802  minmar1val  21806  cramer  21849  cpmatel2  21871  m2cpm  21899  decpmatmul  21930  pmatcollpw1lem2  21933  pmatcollpw1  21934  pmatcollpw2lem  21935  pm2mpcl  21955  mply1topmatcl  21963  mp2pm2mplem2  21965  mp2pm2mplem4  21967  pm2mpghmlem2  21970  pm2mpghmlem1  21971  cayhamlem2  22042  neiint  22264  topssnei  22284  cnrest2  22446  cnprest2  22450  cnt0  22506  cnt1  22510  cnhaus  22514  cncmp  22552  fiuncmp  22564  sscmp  22565  hauscmp  22567  cnconn  22582  unconn  22589  comppfsc  22692  kgen2ss  22715  ptpjopn  22772  ptrescn  22799  qtopss  22875  kqfvima  22890  r0cld  22898  cmphaushmeo  22960  fbssint  22998  fbasrn  23044  filuni  23045  ufilmax  23067  fin1aufil  23092  fmf  23105  fmss  23106  rnelfmlem  23112  rnelfm  23113  fmufil  23119  fmco  23121  flimss2  23132  flimss1  23133  flimrest  23143  cnpflf2  23160  cnpflf  23161  flfcnp  23164  lmflf  23165  supnfcls  23180  fclsss1  23182  fclsss2  23183  cnpfcfi  23200  subgntr  23267  opnsubg  23268  cldsubg  23271  ustuqtop1  23402  ucncn  23446  bldisj  23560  blgt0  23561  bl2in  23562  blss2ps  23565  blss2  23566  xbln0  23576  blssps  23586  blss  23587  lpbl  23668  blcld  23670  blcls  23671  stdbdmopn  23683  metcnp2  23707  txmetcnp  23712  blval2  23727  restmetu  23735  nmoix  23902  nmoi2  23903  nmoeq0  23909  nmotri  23912  metdsge  24021  metds0  24022  metdseq0  24026  icoopnst  24111  iccpnfhmeo  24117  xrhmeo  24118  nmhmcn  24292  cphsqrtcl2  24359  cphsqrtcl3  24360  fmcfil  24445  bcthlem5  24501  cmetcusp1  24526  cssbn  24548  pjth  24612  ovolunnul  24673  volun  24718  voliunlem2  24724  itg2const  24914  iblconst  24991  itgconst  24992  limcvallem  25044  dvcnp2  25093  dvcn  25094  deg1mul3le  25290  deg1tmle  25291  ig1pdvds  25350  coe11  25423  dgrmulc  25441  dvply1  25453  aaliou2  25509  efcvx  25617  tanord  25703  logdivlti  25784  logccv  25827  recxpcl  25839  cxplea  25860  cxple2a  25863  ang180  25973  isosctrlem2  25978  cxp2lim  26135  amgm  26149  muval1  26291  dvdssqf  26296  mumullem2  26338  bcmono  26434  lgsneg  26478  lgsmod  26480  lgsdirprm  26488  lgsdir  26489  lgsdi  26491  brbtwn2  27282  colinearalglem1  27283  colinearalg  27287  axcgrtr  27292  axcontlem2  27342  upgrewlkle2  27982  wlksoneq1eq2  28041  crctcshwlkn0lem5  28188  wspthsnwspthsnon  28290  lppthon  28524  upgriseupth  28580  4cyclusnfrgr  28665  numclwwlk1lem2foa  28727  numclwwlk5  28761  nvmul0or  29021  shless  29730  shlej1  29731  pjspansn  29948  kbmul  30326  homco2  30348  kbass2  30488  fnpreimac  31017  padct  31063  eliccelico  31107  elicoelioo  31108  iocinioc2  31109  difioo  31112  swrdrn2  31235  swrdrn3  31236  xrge0npcan  31312  isarchi2  31448  archiabl  31461  pidlnz  31580  lindssn  31582  ssmxidl  31651  mdetlap1  31785  zarclsiin  31830  pstmfval  31855  fmcncfil  31890  zrhnm  31928  qqhnm  31949  nexple  31986  volfiniune  32207  omsmeas  32299  eulerpartlemb  32344  probinc  32397  cndprob01  32411  signswmnd  32545  cvmsss2  33245  funsseq  33751  sltres  33874  nolt02olem  33906  nolt02o  33907  nogt01o  33908  nosupbnd1lem1  33920  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd1lem6  33925  noinfbnd1lem1  33935  noinfbnd1lem4  33938  noinfbnd1lem6  33940  noinfbnd2  33943  noetainflem3  33951  sltlpss  34096  cofsslt  34097  coinitsslt  34098  cofcutrtime  34102  cgrtriv  34313  5segofs  34317  btwntriv2  34323  btwnxfr  34367  segcon2  34416  brsegle2  34420  seglelin  34427  outsideofeu  34442  lindsenlbs  35781  mblfinlem2  35824  blbnd  35954  rrndstprj2  35998  zerdivemp1x  36114  lsmsat  37029  lsatfixedN  37030  lssat  37037  lkrlsp  37123  lshpkrlem4  37134  cvrcon3b  37298  leat3  37316  atlen0  37331  atnle  37338  atlatmstc  37340  atlatle  37341  cvlcvr1  37360  cvlsupr2  37364  hlsupr2  37408  hlrelat2  37424  cvrexchlem  37440  cvratlem  37442  lnnat  37448  atexchcvrN  37461  1cvratlt  37495  1cvrjat  37496  3atlem3  37506  3atlem7  37510  llni2  37533  atcvrlln2  37540  llnexatN  37542  llncmp  37543  2llnmat  37545  2at0mat0  37546  2atnelpln  37565  llncvrlpln2  37578  2lplnmN  37580  2llnmj  37581  lplncmp  37583  lplnexatN  37584  2llnjaN  37587  lvoli3  37598  islvol2aN  37613  4atlem3a  37618  4atlem4a  37620  4atlem4b  37621  4atlem11  37630  4atlem12  37633  lplncvrlvol2  37636  lvolcmp  37638  2lplnmj  37643  islinei  37761  linepmap  37796  lneq2at  37799  2llnma3r  37809  elpaddn0  37821  elpaddatriN  37824  elpaddat  37825  paddcom  37834  paddss1  37838  paddss2  37839  paddasslem6  37846  paddasslem7  37847  paddasslem10  37850  paddasslem15  37855  pmodlem2  37868  pmodl42N  37872  pmapjoin  37873  atmod1i1m  37879  llnmod1i2  37881  llnexchb2lem  37889  polcon2bN  37941  pclfinclN  37971  poml4N  37974  poml6N  37976  osumcllem11N  37987  osumclN  37988  pmapojoinN  37989  pexmidlem2N  37992  pexmidlem3N  37993  pexmidlem4N  37994  pexmidlem6N  37996  pexmidlem7N  37997  pl42lem2N  38001  pl42lem3N  38002  pl42lem4N  38003  pl42N  38004  lhpexle3lem  38032  lhpmcvr3  38046  lhp2at0nle  38056  lhprelat3N  38061  lauteq  38116  lautco  38118  ltrncoidN  38149  ltrneq2  38169  ltrnnidn  38195  ltrnideq  38196  trlnle  38207  cdlemc  38218  cdlemd4  38222  cdlemd5  38223  cdlemd9  38227  cdlemd  38228  ltrneq3  38229  cdlemefrs29pre00  38416  cdlemefrs29cpre1  38419  cdlemefrs29clN  38420  cdlemefrs32fva  38421  cdlemefr29exN  38423  cdlemefr27cl  38424  cdlemefs27cl  38434  cdlemefs32sn1aw  38435  cdleme32fva  38458  cdleme32d  38465  cdleme32f  38467  cdleme32le  38468  cdleme40n  38489  cdleme41snaw  38497  cdleme17d3  38517  cdleme48fvg  38521  cdlemeg46fvcl  38527  cdlemeg46fgN  38555  cdleme48fgv  38559  ltrniotavalbN  38605  cdlemb3  38627  cdlemg15  38677  cdlemg17dN  38684  trlco  38748  cdlemg44b  38753  ltrncom  38759  trljco  38761  tendococl  38793  tendoplcl  38802  tendoplcom  38803  tendotr  38851  cdlemk36  38934  cdlemk35s-id  38959  cdlemk39s-id  38961  cdlemk19x  38964  cdlemk53b  38977  cdlemk55  38982  cdlemk35u  38985  cdlemk55u  38987  cdlemk39u  38989  cdlemk19u  38991  cdlemk56  38992  tendoex  38996  cdleml5N  39001  dihord2pre  39246  dihord6apre  39277  dihord5b  39280  dihord5apre  39283  dihord  39285  dihmeetlem1N  39311  dihmeetlem2N  39320  dihglbcpreN  39321  dihmeetbN  39324  dihmeetlem4preN  39327  dihmeetlem5  39329  dihmeetlem6  39330  dihmeetlem7N  39331  dihmeetlem10N  39337  dihmeetlem11N  39338  dihmeetlem12N  39339  dihmeetlem13N  39340  dihmeetlem15N  39342  dihmeetlem17N  39344  dihmeetlem18N  39345  dihmeetlem19N  39346  dihmeetALTN  39348  dih1dimatlem0  39349  dihlspsnssN  39353  dvh3dim2  39469  sticksstones1  40109  sticksstones2  40110  sticksstones12  40121  dvdsexpnn  40347  resubcan2  40378  mzpsubst  40577  diophrw  40588  eldioph2lem1  40589  rencldnfi  40650  pellexlem2  40659  pellqrexplicit  40706  infmrgelbi  40707  rmxycomplete  40746  congadd  40795  acongeq  40812  jm2.19  40822  jm2.22  40824  jm2.20nn  40826  jm2.25lem1  40827  jm2.27  40837  jm3.1  40849  lmhmlnmsplit  40919  pwssplit4  40921  hbtlem2  40956  dgraa0p  40981  idomrootle  41027  proot1hash  41032  iocunico  41049  relexpxpmin  41332  brtrclfv2  41342  ntrclsk3  41687  grur1cld  41857  ismnu  41886  suprnmpt  42717  wessf1ornlem  42729  choicefi  42747  supxrgere  42879  supxrgelem  42883  supxrge  42884  infleinflem2  42917  snunioo1  43057  iccintsng  43068  fmul01  43128  lptre2pt  43188  0ellimcdiv  43197  fnlimfvre  43222  limsupmnfuzlem  43274  climisp  43294  limsupgtlem  43325  ibliccsinexp  43499  iblioosinexp  43501  volioc  43520  iblspltprt  43521  stoweidlem20  43568  stoweidlem22  43570  stoweidlem34  43582  stoweidlem44  43592  stoweidlem60  43608  wallispilem3  43615  fourierdlem42  43697  fourierdlem51  43705  fourierdlem54  43708  fourierdlem87  43741  fourierdlem97  43751  ioorrnopnlem  43852  sge0seq  43991  hoicvr  44093  funfocofob  44581  imasetpreimafvbijlemfv  44865  fprmappr  45692  lincresunit3lem3  45826  lindssnlvec  45838  rrx2linesl  46100  line2  46109  itsclc0lem3  46115  itsclc0yqsollem1  46119  itscnhlc0xyqsol  46122  itschlc0xyqsol1  46123  itsclc0  46128  itscnhlinecirc02plem2  46140  itscnhlinecirc02plem3  46141