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  4412  predtrss  6330  frpomin  6348  f1prex  7293  fcofo  7297  soisores  7336  weniso  7365  knatar  7368  ofmpteq  7710  funelss  8053  frrlem10  8301  fprlem1  8306  smocdmdom  8364  nnmord  8627  nnmword  8628  naddasslem1  8690  naddasslem2  8691  difsnen  9057  mapunen  9144  ac6sfi  9254  fipreima  9325  wemaplem2  9519  wemapso2lem  9524  ttrclselem2  9705  en2eqpr  10010  indcardi  10044  acndom  10054  fodomfi2  10063  infmap2  10219  cflim2  10265  coftr  10275  infpssrlem4  10308  fin23lem11  10319  fincssdom  10325  isf32lem9  10363  fin1a2lem9  10410  gchpwdom  10673  gruima  10805  prpssnq  10993  distrlem4pr  11029  dedekind  11391  addcan  11412  addcan2  11413  divmulass  11913  supmul1  12202  uzsupss  12982  xaddass  13293  xleadd1a  13297  xlesubadd  13307  xmulasslem3  13330  xmulass  13331  xadddilem  13338  xadddi  13339  ixxun  13406  icoshftf1o  13519  snunioc  13525  difelfzle  13688  fzo1fzo0n0  13763  ssfzoulel  13808  modmuladd  13969  modifeq2int  13989  modaddmulmod  13994  modsubdir  13996  ltexp2a  14222  leexp2  14227  ltexp2r  14229  exple1  14233  expnlbnd2  14290  mulsubdivbinom2  14318  hashtpg  14542  ccatass  14646  swrdrn3  14714  ccatopth  14777  pfxccatin12lem2a  14788  pfxccat3  14795  cshinj  14874  2cshw  14876  s2f1o  14979  limsupgre  15558  addcn2  15671  mulcn2  15673  binomrisefac  16121  bpolydif  16134  dvdsmodexp  16343  modmulconst  16371  dvdsexp2im  16410  dvdsmod  16412  sadass  16554  gcdass  16630  rplpwr  16641  rpmulgcd2  16739  rpdvds  16743  rpexp  16806  prmdiveq  16870  hashgcdlem  16872  coprimeprodsq  16893  coprimeprodsq2  16894  pythagtriplem3  16903  pcdvdsb  16954  pcgcd1  16962  dvdsprmpweq  16969  pcbc  16985  0ram  17105  ramz2  17109  ramub1lem1  17111  mremre  17681  mrieqv2d  17720  lubun  18596  isnsgrp  18810  issubmnd  18848  frmdss2  18953  submefmnd  18985  sgrp2rid2ex  19020  mulgnn0p1  19182  mulgnnsubcl  19183  mulgneg  19189  mulgdirlem  19202  nmzsubg  19262  ghmmulg  19329  pmtrfv  19553  pmtrmvd  19557  pmtrfb  19566  odmodnn0  19641  oddvdsnn0  19645  odnncl  19646  odmod  19647  oddvds  19648  odeq  19651  odmulgid  19655  odmulg  19657  odmulgeq  19658  odbezout  19659  odf1o1  19673  odf1o2  19674  odngen  19678  odcau  19705  pgpssslw  19715  fislw  19726  lsmless1x  19745  lsmless2x  19746  lsmsubm  19754  lsmmod  19776  lsmmod2  19777  efgsfo  19840  cntzcmn  19941  odadd1  19949  odadd2  19950  odadd  19951  lsmcomx  19957  prdscmnd  19962  gsumconst  20035  ring1eq0  20414  cntzsubrng  20703  cntzsubr  20742  isabvd  20952  rmodislmod  21088  lspss  21142  0lmhm  21198  reslmhm2  21211  pwssplit0  21216  pwssplit1  21217  lbspss  21240  lspfixed  21289  lsmcv  21302  lspsnat  21306  pidlnz  21411  2idlcpblrng  21447  cnfldfunALT  21574  xrsdsreclblem  21600  obselocv  21915  frlmsplit2  21960  frlmsslss2  21962  frlmup4  21988  lindff1  22007  lsslindf  22017  lsslinds  22018  islindf4  22025  issubassa  22054  aspss  22063  coe1subfv  22464  coe1tm  22471  mpomatmul  22640  mamutpos  22652  submaval  22775  mdetdiag  22793  mdetunilem1  22806  mdetunilem3  22808  mdetunilem9  22814  mdetmul  22817  maducoeval2  22834  madurid  22838  minmar1val  22842  cramer  22885  cpmatel2  22907  m2cpm  22935  decpmatmul  22966  pmatcollpw1lem2  22969  pmatcollpw1  22970  pmatcollpw2lem  22971  pm2mpcl  22991  mply1topmatcl  22999  mp2pm2mplem2  23001  mp2pm2mplem4  23003  pm2mpghmlem2  23006  pm2mpghmlem1  23007  cayhamlem2  23078  neiint  23298  topssnei  23318  cnrest2  23480  cnprest2  23484  cnt0  23540  cnt1  23544  cnhaus  23548  cncmp  23586  fiuncmp  23598  sscmp  23599  hauscmp  23601  cnconn  23616  unconn  23623  comppfsc  23726  kgen2ss  23749  ptpjopn  23806  ptrescn  23833  qtopss  23909  kqfvima  23924  r0cld  23932  cmphaushmeo  23994  fbssint  24032  fbasrn  24078  filuni  24079  ufilmax  24101  fin1aufil  24126  fmf  24139  fmss  24140  rnelfmlem  24146  rnelfm  24147  fmufil  24153  fmco  24155  flimss2  24166  flimss1  24167  flimrest  24177  cnpflf2  24194  cnpflf  24195  flfcnp  24198  lmflf  24199  supnfcls  24214  fclsss1  24216  fclsss2  24217  cnpfcfi  24234  subgntr  24301  opnsubg  24302  cldsubg  24305  ustuqtop1  24435  ucncn  24478  bldisj  24592  blgt0  24593  bl2in  24594  blss2ps  24597  blss2  24598  xbln0  24608  blssps  24618  blss  24619  lpbl  24697  blcld  24699  blcls  24700  stdbdmopn  24712  metcnp2  24736  txmetcnp  24741  blval2  24756  restmetu  24764  nmoix  24923  nmoi2  24924  nmoeq0  24930  nmotri  24933  metdsge  25044  metds0  25045  metdseq0  25049  icoopnst  25135  iccpnfhmeo  25141  xrhmeo  25142  nmhmcn  25316  cphsqrtcl2  25382  cphsqrtcl3  25383  fmcfil  25468  bcthlem5  25524  cmetcusp1  25549  cssbn  25571  pjth  25635  ovolunnul  25696  volun  25741  voliunlem2  25747  itg2const  25936  iblconst  26014  itgconst  26015  limcvallem  26067  dvcnp2  26116  dvcn  26117  deg1mul3le  26311  deg1tmle  26312  idomrootle  26367  ig1pdvds  26374  coe11  26447  dgrmulc  26465  dvply1  26482  aaliou2  26540  efcvx  26649  tanord  26740  logdivlti  26822  logccv  26865  recxpcl  26877  cxplea  26898  cxple2a  26901  ang180  27016  isosctrlem2  27021  cxp2lim  27178  amgm  27192  muval1  27334  dvdssqf  27339  mumullem2  27381  bcmono  27478  lgsneg  27522  lgsmod  27524  lgsdirprm  27532  lgsdir  27533  lgsdi  27535  ltsres  27863  nolt02olem  27895  nolt02o  27896  nogt01o  27897  nosupbnd1lem1  27909  nosupbnd1lem4  27912  nosupbnd1lem5  27913  nosupbnd1lem6  27914  noinfbnd1lem1  27924  noinfbnd1lem4  27927  noinfbnd1lem6  27929  noinfbnd2  27932  noetainflem3  27940  ltslpss  28138  cofslts  28148  coinitslts  28149  cofcutrtime  28157  addsass  28235  addsdi  28385  mulsass  28396  ltmuls2  28401  norecdiv  28420  z12bdaylem  28714  brbtwn2  29292  colinearalglem1  29293  colinearalg  29297  axcgrtr  29302  axcontlem2  29352  upgrewlkle2  29993  wlksoneq1eq2  30049  crctcshwlkn0lem5  30200  wspthsnwspthsnon  30302  lppthon  30539  upgriseupth  30595  4cyclusnfrgr  30680  numclwwlk1lem2foa  30742  numclwwlk5  30776  nvmul0or  31039  shless  31748  shlej1  31749  pjspansn  31966  kbmul  32344  homco2  32366  kbass2  32506  fnpreimac  33052  padct  33100  eliccelico  33159  elicoelioo  33160  iocinioc2  33161  difioo  33164  nexple  33214  swrdrn2  33307  xrge0npcan  33371  isarchi2  33536  archiabl  33549  lindssn  33722  ssmxidl  33788  mdetlap1  34247  zarclsiin  34292  pstmfval  34317  fmcncfil  34352  zrhnm  34388  qqhnm  34411  volfiniune  34652  omsmeas  34745  eulerpartlemb  34790  probinc  34843  cndprob01  34857  signswmnd  34976  cvmsss2  35787  funsseq  36281  cgrtriv  36515  5segofs  36519  btwntriv2  36525  btwnxfr  36569  segcon2  36618  brsegle2  36622  seglelin  36629  outsideofeu  36644  nmulss1  36727  ltnmul  36729  nmulle  36730  ltnadd  36731  naddle  36732  nadddi  36737  weiunpo  37017  weiunfr  37019  weiunse  37020  lindsenlbs  38307  mblfinlem2  38350  blbnd  38479  rrndstprj2  38523  zerdivemp1x  38639  lsmsat  39823  lsatfixedN  39824  lssat  39831  lkrlsp  39917  lshpkrlem4  39928  cvrcon3b  40092  leat3  40110  atlen0  40125  atnle  40132  atlatmstc  40134  atlatle  40135  cvlcvr1  40154  cvlsupr2  40158  hlsupr2  40202  hlrelat2  40218  cvrexchlem  40234  cvratlem  40236  lnnat  40242  atexchcvrN  40255  1cvratlt  40289  1cvrjat  40290  3atlem3  40300  3atlem7  40304  llni2  40327  atcvrlln2  40334  llnexatN  40336  llncmp  40337  2llnmat  40339  2at0mat0  40340  2atnelpln  40359  llncvrlpln2  40372  2lplnmN  40374  2llnmj  40375  lplncmp  40377  lplnexatN  40378  2llnjaN  40381  lvoli3  40392  islvol2aN  40407  4atlem3a  40412  4atlem4a  40414  4atlem4b  40415  4atlem11  40424  4atlem12  40427  lplncvrlvol2  40430  lvolcmp  40432  2lplnmj  40437  islinei  40555  linepmap  40590  lneq2at  40593  2llnma3r  40603  elpaddn0  40615  elpaddatriN  40618  elpaddat  40619  paddcom  40628  paddss1  40632  paddss2  40633  paddasslem6  40640  paddasslem7  40641  paddasslem10  40644  paddasslem15  40649  pmodlem2  40662  pmodl42N  40666  pmapjoin  40667  atmod1i1m  40673  llnmod1i2  40675  llnexchb2lem  40683  polcon2bN  40735  pclfinclN  40765  poml4N  40768  poml6N  40770  osumcllem11N  40781  osumclN  40782  pmapojoinN  40783  pexmidlem2N  40786  pexmidlem3N  40787  pexmidlem4N  40788  pexmidlem6N  40790  pexmidlem7N  40791  pl42lem2N  40795  pl42lem3N  40796  pl42lem4N  40797  pl42N  40798  lhpexle3lem  40826  lhpmcvr3  40840  lhp2at0nle  40850  lhprelat3N  40855  lauteq  40910  lautco  40912  ltrncoidN  40943  ltrneq2  40963  ltrnnidn  40989  ltrnideq  40990  trlnle  41001  cdlemc  41012  cdlemd4  41016  cdlemd5  41017  cdlemd9  41021  cdlemd  41022  ltrneq3  41023  cdlemefrs29pre00  41210  cdlemefrs29cpre1  41213  cdlemefrs29clN  41214  cdlemefrs32fva  41215  cdlemefr29exN  41217  cdlemefr27cl  41218  cdlemefs27cl  41228  cdlemefs32sn1aw  41229  cdleme32fva  41252  cdleme32d  41259  cdleme32f  41261  cdleme32le  41262  cdleme40n  41283  cdleme41snaw  41291  cdleme17d3  41311  cdleme48fvg  41315  cdlemeg46fvcl  41321  cdlemeg46fgN  41349  cdleme48fgv  41353  ltrniotavalbN  41399  cdlemb3  41421  cdlemg15  41471  cdlemg17dN  41478  trlco  41542  cdlemg44b  41547  ltrncom  41553  trljco  41555  tendococl  41587  tendoplcl  41596  tendoplcom  41597  tendotr  41645  cdlemk36  41728  cdlemk35s-id  41753  cdlemk39s-id  41755  cdlemk19x  41758  cdlemk53b  41771  cdlemk55  41776  cdlemk35u  41779  cdlemk55u  41781  cdlemk39u  41783  cdlemk19u  41785  cdlemk56  41786  tendoex  41790  cdleml5N  41795  dihord2pre  42040  dihord6apre  42071  dihord5b  42074  dihord5apre  42077  dihord  42079  dihmeetlem1N  42105  dihmeetlem2N  42114  dihglbcpreN  42115  dihmeetbN  42118  dihmeetlem4preN  42121  dihmeetlem5  42123  dihmeetlem6  42124  dihmeetlem7N  42125  dihmeetlem10N  42131  dihmeetlem11N  42132  dihmeetlem12N  42133  dihmeetlem13N  42134  dihmeetlem15N  42136  dihmeetlem17N  42138  dihmeetlem18N  42139  dihmeetlem19N  42140  dihmeetALTN  42142  dih1dimatlem0  42143  dihlspsnssN  42147  dvh3dim2  42263  sticksstones1  42954  sticksstones2  42955  sticksstones12  42966  aks6d1c6isolem1  42982  dvdsexpnn  43135  resubcan2  43190  mzpsubst  43520  diophrw  43531  eldioph2lem1  43532  rencldnfi  43589  pellexlem2  43598  pellqrexplicit  43645  infmrgelbi  43646  rmxycomplete  43685  congadd  43734  acongeq  43751  jm2.19  43761  jm2.22  43763  jm2.20nn  43765  jm2.25lem1  43766  jm2.27  43776  jm3.1  43788  lmhmlnmsplit  43855  pwssplit4  43857  hbtlem2  43892  dgraa0p  43917  proot1hash  43963  iocunico  43979  cantnf2  44093  dflim5  44097  omcl2  44101  tfsconcatrn  44110  nadd2rabex  44154  relexpxpmin  44484  brtrclfv2  44494  ntrclsk3  44837  grur1cld  44997  ismnu  45012  suprnmpt  45933  wessf1ornlem  45944  choicefi  45958  supxrgere  46090  supxrgelem  46094  supxrge  46095  infleinflem2  46127  snunioo1  46269  iccintsng  46280  fmul01  46337  lptre2pt  46395  0ellimcdiv  46404  fnlimfvre  46429  limsupmnfuzlem  46481  climisp  46501  limsupgtlem  46532  ibliccsinexp  46706  iblioosinexp  46708  volioc  46727  iblspltprt  46728  stoweidlem20  46775  stoweidlem22  46777  stoweidlem34  46789  stoweidlem44  46799  stoweidlem60  46815  wallispilem3  46822  fourierdlem42  46904  fourierdlem51  46912  fourierdlem54  46915  fourierdlem87  46948  fourierdlem97  46958  ioorrnopnlem  47059  sge0seq  47201  hoicvr  47303  fsupdm  47597  finfdm  47601  3f1oss1  47853  funfocofob  47856  imasetpreimafvbijlemfv  48192  uhgrimisgrgric  48737  uhgrimgrlim  48793  fprmappr  49166  lincresunit3lem3  49295  lindssnlvec  49307  rrx2linesl  49564  line2  49573  itsclc0lem3  49579  itsclc0yqsollem1  49583  itscnhlc0xyqsol  49586  itschlc0xyqsol1  49587  itsclc0  49592  itscnhlinecirc02plem2  49604  itscnhlinecirc02plem3  49605  uptrlem1  50029  uptr2  50040  setc1onsubc  50421