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  4405  predtrss  6324  frpomin  6342  f1prex  7289  fcofo  7293  soisores  7332  weniso  7361  knatar  7364  ofmpteq  7705  funelss  8048  frrlem10  8298  fprlem1  8303  smocdmdom  8361  nnmord  8624  nnmword  8625  naddasslem1  8687  naddasslem2  8688  difsnen  9061  mapunen  9148  ac6sfi  9258  fipreima  9329  wemaplem2  9523  wemapso2lem  9528  ttrclselem2  9709  en2eqpr  10014  indcardi  10048  acndom  10058  fodomfi2  10067  infmap2  10223  cflim2  10269  coftr  10279  infpssrlem4  10312  fin23lem11  10323  fincssdom  10329  isf32lem9  10367  fin1a2lem9  10414  gchpwdom  10683  gruima  10815  prpssnq  11003  distrlem4pr  11039  dedekind  11401  addcan  11422  addcan2  11423  divmulass  11923  supmul1  12212  uzsupss  12993  xaddass  13305  xleadd1a  13309  xlesubadd  13319  xmulasslem3  13342  xmulass  13343  xadddilem  13350  xadddi  13351  ixxun  13418  icoshftf1o  13531  snunioc  13537  difelfzle  13700  fzo1fzo0n0  13775  ssfzoulel  13820  modmuladd  13981  modifeq2int  14001  modaddmulmod  14006  modsubdir  14008  ltexp2a  14234  leexp2  14239  ltexp2r  14241  exple1  14245  expnlbnd2  14302  mulsubdivbinom2  14330  hashtpg  14554  ccatass  14658  swrdrn3  14726  ccatopth  14789  pfxccatin12lem2a  14800  pfxccat3  14807  cshinj  14886  2cshw  14888  s2f1o  14991  limsupgre  15572  addcn2  15685  mulcn2  15687  binomrisefac  16134  bpolydif  16147  dvdsmodexp  16356  modmulconst  16384  dvdsexp2im  16423  dvdsmod  16425  sadass  16567  gcdass  16643  rplpwr  16654  rpmulgcd2  16752  rpdvds  16756  rpexp  16819  prmdiveq  16883  hashgcdlem  16885  coprimeprodsq  16906  coprimeprodsq2  16907  pythagtriplem3  16916  pcdvdsb  16967  pcgcd1  16975  dvdsprmpweq  16982  pcbc  16998  0ram  17118  ramz2  17122  ramub1lem1  17124  mremre  17694  mrieqv2d  17733  lubun  18609  isnsgrp  18831  issubmnd  18872  frmdss2  18978  submefmnd  19010  sgrp2rid2ex  19045  mulgnn0p1  19214  mulgnnsubcl  19215  mulgneg  19221  mulgdirlem  19234  nmzsubg  19294  ghmmulg  19361  pmtrfv  19585  pmtrmvd  19589  pmtrfb  19598  odmodnn0  19673  oddvdsnn0  19677  odnncl  19678  odmod  19679  oddvds  19680  odeq  19683  odmulgid  19687  odmulg  19689  odmulgeq  19690  odbezout  19691  odf1o1  19705  odf1o2  19706  odngen  19710  odcau  19737  pgpssslw  19747  fislw  19758  lsmless1x  19777  lsmless2x  19778  lsmsubm  19786  lsmmod  19808  lsmmod2  19809  efgsfo  19872  cntzcmn  19973  odadd1  19981  odadd2  19982  odadd  19983  lsmcomx  19989  prdscmnd  19994  gsumconst  20067  ring1eq0  20446  cntzsubrng  20735  cntzsubr  20774  isabvd  20984  rmodislmod  21120  lspss  21174  0lmhm  21230  reslmhm2  21243  pwssplit0  21248  pwssplit1  21249  lbspss  21272  lspfixed  21321  lsmcv  21334  lspsnat  21338  pidlnz  21443  2idlcpblrng  21479  cnfldfunALT  21606  xrsdsreclblem  21632  obselocv  21947  frlmsplit2  21992  frlmsslss2  21994  frlmup4  22020  lindff1  22039  lsslindf  22049  lsslinds  22050  islindf4  22057  lindsenlbs  22070  issubassa  22088  aspss  22097  coe1subfv  22498  coe1tm  22505  mpomatmul  22674  mamutpos  22686  submaval  22809  mdetdiag  22827  mdetunilem1  22840  mdetunilem3  22842  mdetunilem9  22848  mdetmul  22851  maducoeval2  22868  madurid  22872  minmar1val  22876  cramer  22922  cpmatel2  22944  m2cpm  22972  decpmatmul  23003  pmatcollpw1lem2  23006  pmatcollpw1  23007  pmatcollpw2lem  23008  pm2mpcl  23028  mply1topmatcl  23036  mp2pm2mplem2  23038  mp2pm2mplem4  23040  pm2mpghmlem2  23043  pm2mpghmlem1  23044  cayhamlem2  23115  neiint  23335  topssnei  23355  cnrest2  23517  cnprest2  23521  cnt0  23577  cnt1  23581  cnhaus  23585  cncmp  23623  fiuncmp  23635  sscmp  23636  hauscmp  23638  cnconn  23653  unconn  23660  comppfsc  23764  kgen2ss  23787  ptpjopn  23844  ptrescn  23871  qtopss  23947  kqfvima  23962  r0cld  23970  cmphaushmeo  24032  fbssint  24070  fbasrn  24116  filuni  24117  ufilmax  24139  fin1aufil  24164  fmf  24177  fmss  24178  rnelfmlem  24184  rnelfm  24185  fmufil  24191  fmco  24193  flimss2  24204  flimss1  24205  flimrest  24215  cnpflf2  24232  cnpflf  24233  flfcnp  24236  lmflf  24237  supnfcls  24252  fclsss1  24254  fclsss2  24255  cnpfcfi  24272  subgntr  24339  opnsubg  24340  cldsubg  24343  ustuqtop1  24473  ucncn  24516  bldisj  24630  blgt0  24631  bl2in  24632  blss2ps  24635  blss2  24636  xbln0  24646  blssps  24656  blss  24657  lpbl  24735  blcld  24737  blcls  24738  stdbdmopn  24750  metcnp2  24774  txmetcnp  24779  blval2  24794  restmetu  24802  nmoix  24961  nmoi2  24962  nmoeq0  24968  nmotri  24971  metdsge  25082  metds0  25083  metdseq0  25087  icoopnst  25173  iccpnfhmeo  25179  xrhmeo  25180  nmhmcn  25354  cphsqrtcl2  25420  cphsqrtcl3  25421  fmcfil  25506  bcthlem5  25562  cmetcusp1  25587  cssbn  25609  pjth  25673  ovolunnul  25734  volun  25779  voliunlem2  25785  itg2const  25974  iblconst  26052  itgconst  26053  limcvallem  26105  dvcnp2  26154  dvcn  26155  deg1mul3le  26349  deg1tmle  26350  idomrootle  26405  ig1pdvds  26412  coe11  26486  dgrmulc  26504  dvply1  26521  aaliou2  26583  efcvx  26692  tanord  26783  logdivlti  26865  logccv  26908  recxpcl  26920  cxplea  26941  cxple2a  26944  ang180  27059  isosctrlem2  27064  cxp2lim  27221  amgm  27235  muval1  27377  dvdssqf  27382  mumullem2  27424  bcmono  27521  lgsneg  27565  lgsmod  27567  lgsdirprm  27575  lgsdir  27576  lgsdi  27578  ltsres  27906  nolt02olem  27938  nolt02o  27939  nogt01o  27940  nosupbnd1lem1  27952  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd1lem6  27957  noinfbnd1lem1  27967  noinfbnd1lem4  27970  noinfbnd1lem6  27972  noinfbnd2  27975  noetainflem3  27983  ltslpss  28181  cofslts  28191  coinitslts  28192  cofcutrtime  28200  addsass  28278  addsdi  28428  mulsass  28439  ltmuls2  28444  norecdiv  28463  z12bdaylem  28757  brbtwn2  29370  colinearalglem1  29371  colinearalg  29375  axcgrtr  29380  axcontlem2  29430  upgrewlkle2  30074  wlksoneq1eq2  30130  crctcshwlkn0lem5  30290  wspthsnwspthsnon  30392  lppthon  30629  upgriseupth  30695  4cyclusnfrgr  30780  numclwwlk1lem2foa  30842  numclwwlk5  30876  nvmul0or  31139  shless  31848  shlej1  31849  pjspansn  32066  kbmul  32444  homco2  32466  kbass2  32606  fnpreimac  33151  padct  33197  eliccelico  33256  elicoelioo  33257  iocinioc2  33258  difioo  33261  nexple  33311  swrdrn2  33404  xrge0npcan  33468  isarchi2  33633  archiabl  33646  lindssn  33819  ssmxidl  33885  mdetlap1  34344  zarclsiin  34389  pstmfval  34414  fmcncfil  34449  zrhnm  34485  qqhnm  34508  volfiniune  34749  omsmeas  34842  eulerpartlemb  34887  probinc  34940  cndprob01  34954  signswmnd  35073  cvmsss2  35861  funsseq  36355  cgrtriv  36590  5segofs  36594  btwntriv2  36600  btwnxfr  36644  segcon2  36693  brsegle2  36697  seglelin  36704  outsideofeu  36719  nmulss1  36802  ltnmul  36804  nmulle  36805  ltnadd  36806  naddle  36807  nadddi  36812  weiunpo  37092  weiunfr  37094  weiunse  37095  mblfinlem2  38415  blbnd  38545  rrndstprj2  38589  zerdivemp1x  38705  lsmsat  39889  lsatfixedN  39890  lssat  39897  lkrlsp  39983  lshpkrlem4  39994  cvrcon3b  40158  leat3  40176  atlen0  40191  atnle  40198  atlatmstc  40200  atlatle  40201  cvlcvr1  40220  cvlsupr2  40224  hlsupr2  40268  hlrelat2  40284  cvrexchlem  40300  cvratlem  40302  lnnat  40308  atexchcvrN  40321  1cvratlt  40355  1cvrjat  40356  3atlem3  40366  3atlem7  40370  llni2  40393  atcvrlln2  40400  llnexatN  40402  llncmp  40403  2llnmat  40405  2at0mat0  40406  2atnelpln  40425  llncvrlpln2  40438  2lplnmN  40440  2llnmj  40441  lplncmp  40443  lplnexatN  40444  2llnjaN  40447  lvoli3  40458  islvol2aN  40473  4atlem3a  40478  4atlem4a  40480  4atlem4b  40481  4atlem11  40490  4atlem12  40493  lplncvrlvol2  40496  lvolcmp  40498  2lplnmj  40503  islinei  40621  linepmap  40656  lneq2at  40659  2llnma3r  40669  elpaddn0  40681  elpaddatriN  40684  elpaddat  40685  paddcom  40694  paddss1  40698  paddss2  40699  paddasslem6  40706  paddasslem7  40707  paddasslem10  40710  paddasslem15  40715  pmodlem2  40728  pmodl42N  40732  pmapjoin  40733  atmod1i1m  40739  llnmod1i2  40741  llnexchb2lem  40749  polcon2bN  40801  pclfinclN  40831  poml4N  40834  poml6N  40836  osumcllem11N  40847  osumclN  40848  pmapojoinN  40849  pexmidlem2N  40852  pexmidlem3N  40853  pexmidlem4N  40854  pexmidlem6N  40856  pexmidlem7N  40857  pl42lem2N  40861  pl42lem3N  40862  pl42lem4N  40863  pl42N  40864  lhpexle3lem  40892  lhpmcvr3  40906  lhp2at0nle  40916  lhprelat3N  40921  lauteq  40976  lautco  40978  ltrncoidN  41009  ltrneq2  41029  ltrnnidn  41055  ltrnideq  41056  trlnle  41067  cdlemc  41078  cdlemd4  41082  cdlemd5  41083  cdlemd9  41087  cdlemd  41088  ltrneq3  41089  cdlemefrs29pre00  41276  cdlemefrs29cpre1  41279  cdlemefrs29clN  41280  cdlemefrs32fva  41281  cdlemefr29exN  41283  cdlemefr27cl  41284  cdlemefs27cl  41294  cdlemefs32sn1aw  41295  cdleme32fva  41318  cdleme32d  41325  cdleme32f  41327  cdleme32le  41328  cdleme40n  41349  cdleme41snaw  41357  cdleme17d3  41377  cdleme48fvg  41381  cdlemeg46fvcl  41387  cdlemeg46fgN  41415  cdleme48fgv  41419  ltrniotavalbN  41465  cdlemb3  41487  cdlemg15  41537  cdlemg17dN  41544  trlco  41608  cdlemg44b  41613  ltrncom  41619  trljco  41621  tendococl  41653  tendoplcl  41662  tendoplcom  41663  tendotr  41711  cdlemk36  41794  cdlemk35s-id  41819  cdlemk39s-id  41821  cdlemk19x  41824  cdlemk53b  41837  cdlemk55  41842  cdlemk35u  41845  cdlemk55u  41847  cdlemk39u  41849  cdlemk19u  41851  cdlemk56  41852  tendoex  41856  cdleml5N  41861  dihord2pre  42106  dihord6apre  42137  dihord5b  42140  dihord5apre  42143  dihord  42145  dihmeetlem1N  42171  dihmeetlem2N  42180  dihglbcpreN  42181  dihmeetbN  42184  dihmeetlem4preN  42187  dihmeetlem5  42189  dihmeetlem6  42190  dihmeetlem7N  42191  dihmeetlem10N  42197  dihmeetlem11N  42198  dihmeetlem12N  42199  dihmeetlem13N  42200  dihmeetlem15N  42202  dihmeetlem17N  42204  dihmeetlem18N  42205  dihmeetlem19N  42206  dihmeetALTN  42208  dih1dimatlem0  42209  dihlspsnssN  42213  dvh3dim2  42329  sticksstones1  43020  sticksstones2  43021  sticksstones12  43032  aks6d1c6isolem1  43048  dvdsexpnn  43216  resubcan2  43271  mzpsubst  43601  diophrw  43612  eldioph2lem1  43613  rencldnfi  43670  pellexlem2  43679  pellqrexplicit  43726  infmrgelbi  43727  rmxycomplete  43766  congadd  43815  acongeq  43832  jm2.19  43842  jm2.22  43844  jm2.20nn  43846  jm2.25lem1  43847  jm2.27  43857  jm3.1  43869  lmhmlnmsplit  43936  pwssplit4  43938  hbtlem2  43973  dgraa0p  43998  proot1hash  44044  iocunico  44060  cantnf2  44174  dflim5  44178  omcl2  44182  tfsconcatrn  44191  nadd2rabex  44235  relexpxpmin  44565  brtrclfv2  44575  ntrclsk3  44918  grur1cld  45078  ismnu  45093  suprnmpt  46014  wessf1ornlem  46025  choicefi  46039  supxrgere  46171  supxrgelem  46175  supxrge  46176  infleinflem2  46208  snunioo1  46350  iccintsng  46361  fmul01  46418  lptre2pt  46476  0ellimcdiv  46485  fnlimfvre  46510  limsupmnfuzlem  46562  climisp  46582  limsupgtlem  46613  ibliccsinexp  46787  iblioosinexp  46789  volioc  46808  iblspltprt  46809  stoweidlem20  46856  stoweidlem22  46858  stoweidlem34  46870  stoweidlem44  46880  stoweidlem60  46896  wallispilem3  46903  fourierdlem42  46985  fourierdlem51  46993  fourierdlem54  46996  fourierdlem87  47029  fourierdlem97  47039  ioorrnopnlem  47140  sge0seq  47282  hoicvr  47384  fsupdm  47678  finfdm  47682  3f1oss1  47971  funfocofob  47974  imasetpreimafvbijlemfv  48310  uhgrimisgrgric  48855  uhgrimgrlim  48911  fprmappr  49283  lincresunit3lem3  49412  lindssnlvec  49424  rrx2linesl  49681  line2  49690  itsclc0lem3  49696  itsclc0yqsollem1  49700  itscnhlc0xyqsol  49703  itschlc0xyqsol1  49704  itsclc0  49709  itscnhlinecirc02plem2  49721  itscnhlinecirc02plem3  49722  uptrlem1  50144  uptr2  50155  setc1onsubc  50536