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  4385  predtrss  6280  frpomin  6298  f1prex  7232  fcofo  7236  soisores  7275  weniso  7302  knatar  7305  ofmpteq  7647  funelss  7993  frrlem10  8238  fprlem1  8243  smocdmdom  8301  nnmord  8561  nnmword  8562  naddasslem1  8623  naddasslem2  8624  difsnen  8990  mapunen  9077  ac6sfi  9187  fipreima  9261  wemaplem2  9455  wemapso2lem  9460  ttrclselem2  9638  en2eqpr  9920  indcardi  9954  acndom  9964  fodomfi2  9973  infmap2  10130  cflim2  10176  coftr  10186  infpssrlem4  10219  fin23lem11  10230  fincssdom  10236  isf32lem9  10274  fin1a2lem9  10321  gchpwdom  10584  gruima  10716  prpssnq  10904  distrlem4pr  10940  dedekind  11300  addcan  11321  addcan2  11322  divmulass  11823  supmul1  12116  uzsupss  12881  xaddass  13192  xleadd1a  13196  xlesubadd  13206  xmulasslem3  13229  xmulass  13230  xadddilem  13237  xadddi  13238  ixxun  13305  icoshftf1o  13418  snunioc  13424  difelfzle  13586  fzo1fzo0n0  13661  ssfzoulel  13706  modmuladd  13866  modifeq2int  13886  modaddmulmod  13891  modsubdir  13893  ltexp2a  14119  leexp2  14124  ltexp2r  14126  exple1  14130  expnlbnd2  14187  mulsubdivbinom2  14215  hashtpg  14438  ccatass  14542  ccatopth  14669  pfxccatin12lem2a  14680  pfxccat3  14687  cshinj  14764  2cshw  14766  s2f1o  14869  limsupgre  15434  addcn2  15547  mulcn2  15549  binomrisefac  15998  bpolydif  16011  dvdsmodexp  16220  modmulconst  16248  dvdsexp2im  16287  dvdsmod  16289  sadass  16431  gcdass  16507  rplpwr  16518  rpmulgcd2  16616  rpdvds  16620  rpexp  16683  prmdiveq  16747  hashgcdlem  16749  coprimeprodsq  16770  coprimeprodsq2  16771  pythagtriplem3  16780  pcdvdsb  16831  pcgcd1  16839  dvdsprmpweq  16846  pcbc  16862  0ram  16982  ramz2  16986  ramub1lem1  16988  mremre  17557  mrieqv2d  17596  lubun  18472  isnsgrp  18682  issubmnd  18720  frmdss2  18822  submefmnd  18854  sgrp2rid2ex  18889  mulgnn0p1  19052  mulgnnsubcl  19053  mulgneg  19059  mulgdirlem  19072  nmzsubg  19131  ghmmulg  19194  pmtrfv  19418  pmtrmvd  19422  pmtrfb  19431  odmodnn0  19506  oddvdsnn0  19510  odnncl  19511  odmod  19512  oddvds  19513  odeq  19516  odmulgid  19520  odmulg  19522  odmulgeq  19523  odbezout  19524  odf1o1  19538  odf1o2  19539  odngen  19543  odcau  19570  pgpssslw  19580  fislw  19591  lsmless1x  19610  lsmless2x  19611  lsmsubm  19619  lsmmod  19641  lsmmod2  19642  efgsfo  19705  cntzcmn  19806  odadd1  19814  odadd2  19815  odadd  19816  lsmcomx  19822  prdscmnd  19827  gsumconst  19900  ring1eq0  20270  cntzsubrng  20535  cntzsubr  20574  isabvd  20780  rmodislmod  20916  lspss  20970  0lmhm  21027  reslmhm2  21040  pwssplit0  21045  pwssplit1  21046  lbspss  21069  lspfixed  21118  lsmcv  21131  lspsnat  21135  2idlcpblrng  21261  cnfldfunALT  21359  cnfldfunALTOLD  21372  xrsdsreclblem  21402  obselocv  21718  frlmsplit2  21763  frlmsslss2  21765  frlmup4  21791  lindff1  21810  lsslindf  21820  lsslinds  21821  islindf4  21828  issubassa  21857  aspss  21866  coe1subfv  22241  coe1tm  22248  mpomatmul  22421  mamutpos  22433  submaval  22556  mdetdiag  22574  mdetunilem1  22587  mdetunilem3  22589  mdetunilem9  22595  mdetmul  22598  maducoeval2  22615  madurid  22619  minmar1val  22623  cramer  22666  cpmatel2  22688  m2cpm  22716  decpmatmul  22747  pmatcollpw1lem2  22750  pmatcollpw1  22751  pmatcollpw2lem  22752  pm2mpcl  22772  mply1topmatcl  22780  mp2pm2mplem2  22782  mp2pm2mplem4  22784  pm2mpghmlem2  22787  pm2mpghmlem1  22788  cayhamlem2  22859  neiint  23079  topssnei  23099  cnrest2  23261  cnprest2  23265  cnt0  23321  cnt1  23325  cnhaus  23329  cncmp  23367  fiuncmp  23379  sscmp  23380  hauscmp  23382  cnconn  23397  unconn  23404  comppfsc  23507  kgen2ss  23530  ptpjopn  23587  ptrescn  23614  qtopss  23690  kqfvima  23705  r0cld  23713  cmphaushmeo  23775  fbssint  23813  fbasrn  23859  filuni  23860  ufilmax  23882  fin1aufil  23907  fmf  23920  fmss  23921  rnelfmlem  23927  rnelfm  23928  fmufil  23934  fmco  23936  flimss2  23947  flimss1  23948  flimrest  23958  cnpflf2  23975  cnpflf  23976  flfcnp  23979  lmflf  23980  supnfcls  23995  fclsss1  23997  fclsss2  23998  cnpfcfi  24015  subgntr  24082  opnsubg  24083  cldsubg  24086  ustuqtop1  24216  ucncn  24259  bldisj  24373  blgt0  24374  bl2in  24375  blss2ps  24378  blss2  24379  xbln0  24389  blssps  24399  blss  24400  lpbl  24478  blcld  24480  blcls  24481  stdbdmopn  24493  metcnp2  24517  txmetcnp  24522  blval2  24537  restmetu  24545  nmoix  24704  nmoi2  24705  nmoeq0  24711  nmotri  24714  metdsge  24825  metds0  24826  metdseq0  24830  icoopnst  24916  iccpnfhmeo  24922  xrhmeo  24923  nmhmcn  25097  cphsqrtcl2  25163  cphsqrtcl3  25164  fmcfil  25249  bcthlem5  25305  cmetcusp1  25330  cssbn  25352  pjth  25416  ovolunnul  25477  volun  25522  voliunlem2  25528  itg2const  25717  iblconst  25795  itgconst  25796  limcvallem  25848  dvcnp2  25897  dvcn  25898  deg1mul3le  26092  deg1tmle  26093  idomrootle  26148  ig1pdvds  26155  coe11  26228  dgrmulc  26246  dvply1  26260  aaliou2  26317  efcvx  26427  tanord  26515  logdivlti  26597  logccv  26640  recxpcl  26652  cxplea  26673  cxple2a  26676  ang180  26791  isosctrlem2  26796  cxp2lim  26954  amgm  26968  muval1  27110  dvdssqf  27115  mumullem2  27157  bcmono  27254  lgsneg  27298  lgsmod  27300  lgsdirprm  27308  lgsdir  27309  lgsdi  27311  ltsres  27640  nolt02olem  27672  nolt02o  27673  nogt01o  27674  nosupbnd1lem1  27686  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd1lem6  27691  noinfbnd1lem1  27701  noinfbnd1lem4  27704  noinfbnd1lem6  27706  noinfbnd2  27709  noetainflem3  27717  ltslpss  27914  cofslts  27924  coinitslts  27925  cofcutrtime  27933  addsass  28011  addsdi  28161  mulsass  28172  ltmuls2  28177  norecdiv  28196  z12bdaylem  28490  brbtwn2  28988  colinearalglem1  28989  colinearalg  28993  axcgrtr  28998  axcontlem2  29048  upgrewlkle2  29690  wlksoneq1eq2  29746  crctcshwlkn0lem5  29897  wspthsnwspthsnon  29999  lppthon  30236  upgriseupth  30292  4cyclusnfrgr  30377  numclwwlk1lem2foa  30439  numclwwlk5  30473  nvmul0or  30736  shless  31445  shlej1  31446  pjspansn  31663  kbmul  32041  homco2  32063  kbass2  32203  fnpreimac  32758  padct  32806  eliccelico  32865  elicoelioo  32866  iocinioc2  32867  difioo  32870  nexple  32932  swrdrn2  33029  swrdrn3  33030  xrge0npcan  33095  isarchi2  33261  archiabl  33274  pidlnz  33451  lindssn  33453  ssmxidl  33549  mdetlap1  33986  zarclsiin  34031  pstmfval  34056  fmcncfil  34091  zrhnm  34127  qqhnm  34150  volfiniune  34390  omsmeas  34483  eulerpartlemb  34528  probinc  34581  cndprob01  34595  signswmnd  34717  cvmsss2  35472  funsseq  35966  cgrtriv  36200  5segofs  36204  btwntriv2  36210  btwnxfr  36254  segcon2  36303  brsegle2  36307  seglelin  36314  outsideofeu  36329  weiunpo  36663  weiunfr  36665  weiunse  36666  lindsenlbs  37950  mblfinlem2  37993  blbnd  38122  rrndstprj2  38166  zerdivemp1x  38282  lsmsat  39468  lsatfixedN  39469  lssat  39476  lkrlsp  39562  lshpkrlem4  39573  cvrcon3b  39737  leat3  39755  atlen0  39770  atnle  39777  atlatmstc  39779  atlatle  39780  cvlcvr1  39799  cvlsupr2  39803  hlsupr2  39847  hlrelat2  39863  cvrexchlem  39879  cvratlem  39881  lnnat  39887  atexchcvrN  39900  1cvratlt  39934  1cvrjat  39935  3atlem3  39945  3atlem7  39949  llni2  39972  atcvrlln2  39979  llnexatN  39981  llncmp  39982  2llnmat  39984  2at0mat0  39985  2atnelpln  40004  llncvrlpln2  40017  2lplnmN  40019  2llnmj  40020  lplncmp  40022  lplnexatN  40023  2llnjaN  40026  lvoli3  40037  islvol2aN  40052  4atlem3a  40057  4atlem4a  40059  4atlem4b  40060  4atlem11  40069  4atlem12  40072  lplncvrlvol2  40075  lvolcmp  40077  2lplnmj  40082  islinei  40200  linepmap  40235  lneq2at  40238  2llnma3r  40248  elpaddn0  40260  elpaddatriN  40263  elpaddat  40264  paddcom  40273  paddss1  40277  paddss2  40278  paddasslem6  40285  paddasslem7  40286  paddasslem10  40289  paddasslem15  40294  pmodlem2  40307  pmodl42N  40311  pmapjoin  40312  atmod1i1m  40318  llnmod1i2  40320  llnexchb2lem  40328  polcon2bN  40380  pclfinclN  40410  poml4N  40413  poml6N  40415  osumcllem11N  40426  osumclN  40427  pmapojoinN  40428  pexmidlem2N  40431  pexmidlem3N  40432  pexmidlem4N  40433  pexmidlem6N  40435  pexmidlem7N  40436  pl42lem2N  40440  pl42lem3N  40441  pl42lem4N  40442  pl42N  40443  lhpexle3lem  40471  lhpmcvr3  40485  lhp2at0nle  40495  lhprelat3N  40500  lauteq  40555  lautco  40557  ltrncoidN  40588  ltrneq2  40608  ltrnnidn  40634  ltrnideq  40635  trlnle  40646  cdlemc  40657  cdlemd4  40661  cdlemd5  40662  cdlemd9  40666  cdlemd  40667  ltrneq3  40668  cdlemefrs29pre00  40855  cdlemefrs29cpre1  40858  cdlemefrs29clN  40859  cdlemefrs32fva  40860  cdlemefr29exN  40862  cdlemefr27cl  40863  cdlemefs27cl  40873  cdlemefs32sn1aw  40874  cdleme32fva  40897  cdleme32d  40904  cdleme32f  40906  cdleme32le  40907  cdleme40n  40928  cdleme41snaw  40936  cdleme17d3  40956  cdleme48fvg  40960  cdlemeg46fvcl  40966  cdlemeg46fgN  40994  cdleme48fgv  40998  ltrniotavalbN  41044  cdlemb3  41066  cdlemg15  41116  cdlemg17dN  41123  trlco  41187  cdlemg44b  41192  ltrncom  41198  trljco  41200  tendococl  41232  tendoplcl  41241  tendoplcom  41242  tendotr  41290  cdlemk36  41373  cdlemk35s-id  41398  cdlemk39s-id  41400  cdlemk19x  41403  cdlemk53b  41416  cdlemk55  41421  cdlemk35u  41424  cdlemk55u  41426  cdlemk39u  41428  cdlemk19u  41430  cdlemk56  41431  tendoex  41435  cdleml5N  41440  dihord2pre  41685  dihord6apre  41716  dihord5b  41719  dihord5apre  41722  dihord  41724  dihmeetlem1N  41750  dihmeetlem2N  41759  dihglbcpreN  41760  dihmeetbN  41763  dihmeetlem4preN  41766  dihmeetlem5  41768  dihmeetlem6  41769  dihmeetlem7N  41770  dihmeetlem10N  41776  dihmeetlem11N  41777  dihmeetlem12N  41778  dihmeetlem13N  41779  dihmeetlem15N  41781  dihmeetlem17N  41783  dihmeetlem18N  41784  dihmeetlem19N  41785  dihmeetALTN  41787  dih1dimatlem0  41788  dihlspsnssN  41792  dvh3dim2  41908  sticksstones1  42599  sticksstones2  42600  sticksstones12  42611  aks6d1c6isolem1  42627  dvdsexpnn  42779  resubcan2  42834  mzpsubst  43194  diophrw  43205  eldioph2lem1  43206  rencldnfi  43267  pellexlem2  43276  pellqrexplicit  43323  infmrgelbi  43324  rmxycomplete  43363  congadd  43412  acongeq  43429  jm2.19  43439  jm2.22  43441  jm2.20nn  43443  jm2.25lem1  43444  jm2.27  43454  jm3.1  43466  lmhmlnmsplit  43533  pwssplit4  43535  hbtlem2  43570  dgraa0p  43595  proot1hash  43641  iocunico  43657  cantnf2  43771  dflim5  43775  omcl2  43779  tfsconcatrn  43788  nadd2rabex  43832  relexpxpmin  44162  brtrclfv2  44172  ntrclsk3  44515  grur1cld  44677  ismnu  44706  suprnmpt  45622  wessf1ornlem  45633  choicefi  45647  supxrgere  45781  supxrgelem  45785  supxrge  45786  infleinflem2  45818  snunioo1  45960  iccintsng  45971  fmul01  46028  lptre2pt  46086  0ellimcdiv  46095  fnlimfvre  46120  limsupmnfuzlem  46172  climisp  46192  limsupgtlem  46223  ibliccsinexp  46397  iblioosinexp  46399  volioc  46418  iblspltprt  46419  stoweidlem20  46466  stoweidlem22  46468  stoweidlem34  46480  stoweidlem44  46490  stoweidlem60  46506  wallispilem3  46513  fourierdlem42  46595  fourierdlem51  46603  fourierdlem54  46606  fourierdlem87  46639  fourierdlem97  46649  ioorrnopnlem  46750  sge0seq  46892  hoicvr  46994  fsupdm  47288  finfdm  47292  3f1oss1  47535  funfocofob  47538  imasetpreimafvbijlemfv  47874  uhgrimisgrgric  48419  uhgrimgrlim  48475  fprmappr  48833  lincresunit3lem3  48962  lindssnlvec  48974  rrx2linesl  49231  line2  49240  itsclc0lem3  49246  itsclc0yqsollem1  49250  itscnhlc0xyqsol  49253  itschlc0xyqsol1  49254  itsclc0  49259  itscnhlinecirc02plem2  49271  itscnhlinecirc02plem3  49272  uptrlem1  49697  uptr2  49708  setc1onsubc  50089