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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl13  1269  simpl23  1272  simpl33  1275  simp1l3  1287  simp2l3  1293  simp3l3  1299  3anandirs  1501  2nreu  4401  predtrss  6325  frpomin  6343  f1prex  7292  fcofo  7296  soisores  7335  weniso  7364  knatar  7367  ofmpteq  7716  funelss  8058  frrlem10  8316  fprlem1  8321  smocdmdom  8379  nnmord  8644  nnmword  8645  naddasslem1  8707  naddasslem2  8708  difsnen  9081  mapunen  9168  ac6sfi  9278  fipreima  9350  wemaplem2  9544  wemapso2lem  9549  ttrclselem2  9730  en2eqpr  10089  indcardi  10123  acndom  10133  fodomfi2  10142  infmap2  10298  cflim2  10344  coftr  10354  infpssrlem4  10387  fin23lem11  10398  fincssdom  10404  isf32lem9  10442  fin1a2lem9  10489  gchpwdom  10758  gruima  10890  prpssnq  11078  distrlem4pr  11114  dedekind  11476  addcan  11497  addcan2  11498  divmulass  12000  supmul1  12289  uzsupss  13070  xaddass  13382  xleadd1a  13386  xlesubadd  13396  xmulasslem3  13419  xmulass  13420  xadddilem  13427  xadddi  13428  ixxun  13495  icoshftf1o  13608  snunioc  13614  difelfzle  13778  fzo1fzo0n0  13853  ssfzoulel  13898  modmuladd  14059  modifeq2int  14079  modaddmulmod  14084  modsubdir  14086  ltexp2a  14312  leexp2  14317  ltexp2r  14319  exple1  14323  expnlbnd2  14381  mulsubdivbinom2  14409  hashtpg  14633  ccatass  14737  swrdrn3  14806  ccatopth  14869  pfxccatin12lem2a  14880  pfxccat3  14887  cshinj  14966  2cshw  14968  s2f1o  15072  limsupgre  15653  addcn2  15766  mulcn2  15768  binomrisefac  16213  bpolydif  16226  dvdsmodexp  16435  modmulconst  16463  dvdsexp2im  16502  dvdsmod  16504  sadass  16646  gcdass  16725  rplpwr  16737  dvdsexpnn  16745  rpmulgcd2  16836  rpdvds  16840  rpexp  16903  prmdiveq  16968  hashgcdlem  16970  coprimeprodsq  16991  coprimeprodsq2  16992  pythagtriplem3  17001  pcdvdsb  17052  pcgcd1  17060  dvdsprmpweq  17067  pcbc  17083  0ram  17203  ramz2  17207  ramub1lem1  17209  mremre  17779  mrieqv2d  17818  lubun  18694  isnsgrp  18917  issubmnd  18958  frmdss2  19064  submefmnd  19096  sgrp2rid2ex  19131  mulgnn0p1  19300  mulgnnsubcl  19301  mulgneg  19307  mulgdirlem  19320  nmzsubg  19380  ghmmulg  19447  pmtrfv  19671  pmtrmvd  19675  pmtrfb  19684  odmodnn0  19759  oddvdsnn0  19763  odnncl  19764  odmod  19765  oddvds  19766  odeq  19769  odmulgid  19773  odmulg  19775  odmulgeq  19776  odbezout  19777  odf1o1  19791  odf1o2  19792  odngen  19796  odcau  19823  pgpssslw  19833  fislw  19844  lsmless1x  19863  lsmless2x  19864  lsmsubm  19872  lsmmod  19894  lsmmod2  19895  efgsfo  19958  cntzcmn  20059  odadd1  20067  odadd2  20068  odadd  20069  lsmcomx  20075  prdscmnd  20080  gsumconst  20153  ring1eq0  20534  cntzsubrng  20824  cntzsubr  20863  isabvd  21074  rmodislmod  21210  lspss  21264  0lmhm  21320  reslmhm2  21333  pwssplit0  21338  pwssplit1  21339  lbspss  21362  lspfixed  21411  lsmcv  21424  lspsnat  21428  pidlnz  21533  2idlcpblrng  21570  cnfldfunALT  21698  xrsdsreclblem  21724  obselocv  22039  frlmsplit2  22084  frlmsslss2  22086  frlmup4  22112  lindff1  22131  lsslindf  22141  lsslinds  22142  islindf4  22149  lindsenlbs  22162  issubassa  22180  aspss  22189  coe1subfv  22590  coe1tm  22597  mpomatmul  22766  mamutpos  22778  submaval  22901  mdetdiag  22919  mdetunilem1  22932  mdetunilem3  22934  mdetunilem9  22940  mdetmul  22943  maducoeval2  22960  madurid  22964  minmar1val  22968  cramer  23014  cpmatel2  23036  m2cpm  23064  decpmatmul  23095  pmatcollpw1lem2  23098  pmatcollpw1  23099  pmatcollpw2lem  23100  pm2mpcl  23120  mply1topmatcl  23128  mp2pm2mplem2  23130  mp2pm2mplem4  23132  pm2mpghmlem2  23135  pm2mpghmlem1  23136  cayhamlem2  23207  neiint  23427  topssnei  23447  cnrest2  23609  cnprest2  23613  cnt0  23669  cnt1  23673  cnhaus  23677  cncmp  23715  fiuncmp  23727  sscmp  23728  hauscmp  23730  cnconn  23745  unconn  23752  comppfsc  23856  kgen2ss  23879  ptpjopn  23936  ptrescn  23963  qtopss  24039  kqfvima  24054  r0cld  24062  cmphaushmeo  24124  fbssint  24162  fbasrn  24208  filuni  24209  ufilmax  24231  fin1aufil  24256  fmf  24269  fmss  24270  rnelfmlem  24276  rnelfm  24277  fmufil  24283  fmco  24285  flimss2  24296  flimss1  24297  flimrest  24307  cnpflf2  24324  cnpflf  24325  flfcnp  24328  lmflf  24329  supnfcls  24344  fclsss1  24346  fclsss2  24347  cnpfcfi  24364  subgntr  24431  opnsubg  24432  cldsubg  24435  ustuqtop1  24565  ucncn  24608  bldisj  24722  blgt0  24723  bl2in  24724  blss2ps  24727  blss2  24728  xbln0  24738  blssps  24748  blss  24749  lpbl  24827  blcld  24829  blcls  24830  stdbdmopn  24842  metcnp2  24866  txmetcnp  24871  blval2  24886  restmetu  24894  nmoix  25053  nmoi2  25054  nmoeq0  25060  nmotri  25063  metdsge  25174  metds0  25175  metdseq0  25179  icoopnst  25265  iccpnfhmeo  25271  xrhmeo  25272  nmhmcn  25446  cphsqrtcl2  25512  cphsqrtcl3  25513  fmcfil  25598  bcthlem5  25654  cmetcusp1  25679  cssbn  25701  pjth  25765  ovolunnul  25826  volun  25871  voliunlem2  25877  itg2const  26066  iblconst  26143  itgconst  26144  limcvallem  26196  dvcnp2  26245  dvcn  26246  deg1mul3le  26440  deg1tmle  26441  idomrootle  26496  ig1pdvds  26503  coe11  26577  dgrmulc  26595  dvply1  26610  aaliou2  26672  efcvx  26781  tanord  26871  logdivlti  26953  logccv  26996  recxpcl  27008  cxplea  27029  cxple2a  27032  ang180  27147  isosctrlem2  27152  cxp2lim  27309  amgm  27323  muval1  27465  dvdssqf  27470  mumullem2  27512  bcmono  27609  lgsneg  27653  lgsmod  27655  lgsdirprm  27663  lgsdir  27664  lgsdi  27666  ltsres  28024  nolt02olem  28056  nolt02o  28057  nogt01o  28058  nosupbnd1lem1  28070  nosupbnd1lem4  28073  nosupbnd1lem5  28074  nosupbnd1lem6  28075  noinfbnd1lem1  28085  noinfbnd1lem4  28088  noinfbnd1lem6  28090  noinfbnd2  28093  noetainflem3  28101  ltslpss  28299  cofslts  28309  coinitslts  28310  cofcutrtime  28318  addsass  28396  addsdi  28546  mulsass  28557  ltmuls2  28562  norecdiv  28581  z12bdaylem  28875  brbtwn2  29488  colinearalglem1  29489  colinearalg  29493  axcgrtr  29498  axcontlem2  29548  upgrewlkle2  30192  wlksoneq1eq2  30248  crctcshwlkn0lem5  30408  wspthsnwspthsnon  30510  lppthon  30747  upgriseupth  30813  4cyclusnfrgr  30898  numclwwlk1lem2foa  30960  numclwwlk5  30994  nvmul0or  31257  shless  31966  shlej1  31967  pjspansn  32184  kbmul  32562  homco2  32584  kbass2  32724  fnpreimac  33311  padct  33357  eliccelico  33415  elicoelioo  33416  iocinioc2  33417  difioo  33420  nexple  33470  swrdrn2  33563  xrge0npcan  33627  isarchi2  33792  archiabl  33805  lindssn  33979  ssmxidl  34045  mdetlap1  34504  zarclsiin  34549  pstmfval  34574  fmcncfil  34609  zrhnm  34645  qqhnm  34668  volfiniune  34909  omsmeas  35001  eulerpartlemb  35046  probinc  35099  cndprob01  35113  signswmnd  35232  cvmsss2  36125  funsseq  36625  cgrtriv  36859  5segofs  36863  btwntriv2  36869  btwnxfr  36913  segcon2  36962  brsegle2  36966  seglelin  36973  outsideofeu  36988  nmulss1  37055  ltnmul  37057  nmulle  37058  ltnadd  37059  naddle  37060  nadddi  37065  weiunpo  37345  weiunfr  37347  weiunse  37348  mblfinlem2  38669  blbnd  38814  rrndstprj2  38858  zerdivemp1x  38974  lsmsat  40158  lsatfixedN  40159  lssat  40166  lkrlsp  40252  lshpkrlem4  40263  cvrcon3b  40427  leat3  40445  atlen0  40460  atnle  40467  atlatmstc  40469  atlatle  40470  cvlcvr1  40489  cvlsupr2  40493  hlsupr2  40537  hlrelat2  40553  cvrexchlem  40569  cvratlem  40571  lnnat  40577  atexchcvrN  40590  1cvratlt  40624  1cvrjat  40625  3atlem3  40635  3atlem7  40639  llni2  40662  atcvrlln2  40669  llnexatN  40671  llncmp  40672  2llnmat  40674  2at0mat0  40675  2atnelpln  40694  llncvrlpln2  40707  2lplnmN  40709  2llnmj  40710  lplncmp  40712  lplnexatN  40713  2llnjaN  40716  lvoli3  40727  islvol2aN  40742  4atlem3a  40747  4atlem4a  40749  4atlem4b  40750  4atlem11  40759  4atlem12  40762  lplncvrlvol2  40765  lvolcmp  40767  2lplnmj  40772  islinei  40890  linepmap  40925  lneq2at  40928  2llnma3r  40938  elpaddn0  40950  elpaddatriN  40953  elpaddat  40954  paddcom  40963  paddss1  40967  paddss2  40968  paddasslem6  40975  paddasslem7  40976  paddasslem10  40979  paddasslem15  40984  pmodlem2  40997  pmodl42N  41001  pmapjoin  41002  atmod1i1m  41008  llnmod1i2  41010  llnexchb2lem  41018  polcon2bN  41070  pclfinclN  41100  poml4N  41103  poml6N  41105  osumcllem11N  41116  osumclN  41117  pmapojoinN  41118  pexmidlem2N  41121  pexmidlem3N  41122  pexmidlem4N  41123  pexmidlem6N  41125  pexmidlem7N  41126  pl42lem2N  41130  pl42lem3N  41131  pl42lem4N  41132  pl42N  41133  lhpexle3lem  41161  lhpmcvr3  41175  lhp2at0nle  41185  lhprelat3N  41190  lauteq  41245  lautco  41247  ltrncoidN  41278  ltrneq2  41298  ltrnnidn  41324  ltrnideq  41325  trlnle  41336  cdlemc  41347  cdlemd4  41351  cdlemd5  41352  cdlemd9  41356  cdlemd  41357  ltrneq3  41358  cdlemefrs29pre00  41545  cdlemefrs29cpre1  41548  cdlemefrs29clN  41549  cdlemefrs32fva  41550  cdlemefr29exN  41552  cdlemefr27cl  41553  cdlemefs27cl  41563  cdlemefs32sn1aw  41564  cdleme32fva  41587  cdleme32d  41594  cdleme32f  41596  cdleme32le  41597  cdleme40n  41618  cdleme41snaw  41626  cdleme17d3  41646  cdleme48fvg  41650  cdlemeg46fvcl  41656  cdlemeg46fgN  41684  cdleme48fgv  41688  ltrniotavalbN  41734  cdlemb3  41756  cdlemg15  41806  cdlemg17dN  41813  trlco  41877  cdlemg44b  41882  ltrncom  41888  trljco  41890  tendococl  41922  tendoplcl  41931  tendoplcom  41932  tendotr  41980  cdlemk36  42063  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk19x  42093  cdlemk53b  42106  cdlemk55  42111  cdlemk35u  42114  cdlemk55u  42116  cdlemk39u  42118  cdlemk19u  42120  cdlemk56  42121  tendoex  42125  cdleml5N  42130  dihord2pre  42375  dihord6apre  42406  dihord5b  42409  dihord5apre  42412  dihord  42414  dihmeetlem1N  42440  dihmeetlem2N  42449  dihglbcpreN  42450  dihmeetbN  42453  dihmeetlem4preN  42456  dihmeetlem5  42458  dihmeetlem6  42459  dihmeetlem7N  42460  dihmeetlem10N  42466  dihmeetlem11N  42467  dihmeetlem12N  42468  dihmeetlem13N  42469  dihmeetlem15N  42471  dihmeetlem17N  42473  dihmeetlem18N  42474  dihmeetlem19N  42475  dihmeetALTN  42477  dih1dimatlem0  42478  dihlspsnssN  42482  dvh3dim2  42598  sticksstones1  43289  sticksstones2  43290  sticksstones12  43301  aks6d1c6isolem1  43317  resubcan2  43532  mzpsubst  43852  diophrw  43863  eldioph2lem1  43864  rencldnfi  43921  pellexlem2  43930  pellqrexplicit  43977  infmrgelbi  43978  rmxycomplete  44017  congadd  44066  acongeq  44083  jm2.19  44093  jm2.22  44095  jm2.20nn  44097  jm2.25lem1  44098  jm2.27  44108  jm3.1  44120  lmhmlnmsplit  44182  pwssplit4  44184  hbtlem2  44219  dgraa0p  44244  proot1hash  44290  iocunico  44306  cantnf2  44420  dflim5  44424  omcl2  44428  tfsconcatrn  44437  nadd2rabex  44481  relexpxpmin  44810  brtrclfv2  44820  ntrclsk3  45163  grur1cld  45323  ismnu  45338  suprnmpt  46282  wessf1ornlem  46293  choicefi  46307  supxrgere  46438  supxrgelem  46442  supxrge  46443  infleinflem2  46475  snunioo1  46617  iccintsng  46628  fmul01  46685  lptre2pt  46743  0ellimcdiv  46752  fnlimfvre  46777  limsupmnfuzlem  46829  climisp  46849  limsupgtlem  46880  ibliccsinexp  47054  iblioosinexp  47056  volioc  47075  iblspltprt  47076  stoweidlem20  47123  stoweidlem22  47125  stoweidlem34  47137  stoweidlem44  47147  stoweidlem60  47163  wallispilem3  47170  fourierdlem42  47252  fourierdlem51  47260  fourierdlem54  47263  fourierdlem87  47296  fourierdlem97  47306  ioorrnopnlem  47407  sge0seq  47549  hoicvr  47651  fsupdm  47945  finfdm  47949  3f1oss1  48238  funfocofob  48241  imasetpreimafvbijlemfv  48577  uhgrimisgrgric  49122  uhgrimgrlim  49178  fprmappr  49550  lincresunit3lem3  49679  lindssnlvec  49691  rrx2linesl  49948  itsclc0lem3  49963  itsclc0yqsollem1  49967  itscnhlc0xyqsol  49970  itschlc0xyqsol1  49971  itsclc0  49976  itscnhlinecirc02plem2  49988  itscnhlinecirc02plem3  49989  uptrlem1  50419  uptr2  50430  setc1onsubc  50833