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  4398  predtrss  6288  frpomin  6306  f1prex  7240  fcofo  7244  soisores  7283  weniso  7310  knatar  7313  ofmpteq  7655  funelss  8001  frrlem10  8247  fprlem1  8252  smocdmdom  8310  nnmord  8570  nnmword  8571  naddasslem1  8632  naddasslem2  8633  difsnen  8999  mapunen  9086  ac6sfi  9196  fipreima  9270  wemaplem2  9464  wemapso2lem  9469  ttrclselem2  9647  en2eqpr  9929  indcardi  9963  acndom  9973  fodomfi2  9982  infmap2  10139  cflim2  10185  coftr  10195  infpssrlem4  10228  fin23lem11  10239  fincssdom  10245  isf32lem9  10283  fin1a2lem9  10330  gchpwdom  10593  gruima  10725  prpssnq  10913  distrlem4pr  10949  dedekind  11308  addcan  11329  addcan2  11330  divmulass  11831  supmul1  12123  uzsupss  12865  xaddass  13176  xleadd1a  13180  xlesubadd  13190  xmulasslem3  13213  xmulass  13214  xadddilem  13221  xadddi  13222  ixxun  13289  icoshftf1o  13402  snunioc  13408  difelfzle  13569  fzo1fzo0n0  13643  ssfzoulel  13688  modmuladd  13848  modifeq2int  13868  modaddmulmod  13873  modsubdir  13875  ltexp2a  14101  leexp2  14106  ltexp2r  14108  exple1  14112  expnlbnd2  14169  mulsubdivbinom2  14197  hashtpg  14420  ccatass  14524  ccatopth  14651  pfxccatin12lem2a  14662  pfxccat3  14669  cshinj  14746  2cshw  14748  s2f1o  14851  limsupgre  15416  addcn2  15529  mulcn2  15531  binomrisefac  15977  bpolydif  15990  dvdsmodexp  16199  modmulconst  16227  dvdsexp2im  16266  dvdsmod  16268  sadass  16410  gcdass  16486  rplpwr  16497  rpmulgcd2  16595  rpdvds  16599  rpexp  16661  prmdiveq  16725  hashgcdlem  16727  coprimeprodsq  16748  coprimeprodsq2  16749  pythagtriplem3  16758  pcdvdsb  16809  pcgcd1  16817  dvdsprmpweq  16824  pcbc  16840  0ram  16960  ramz2  16964  ramub1lem1  16966  mremre  17535  mrieqv2d  17574  lubun  18450  isnsgrp  18660  issubmnd  18698  frmdss2  18800  submefmnd  18832  sgrp2rid2ex  18864  mulgnn0p1  19027  mulgnnsubcl  19028  mulgneg  19034  mulgdirlem  19047  nmzsubg  19106  ghmmulg  19169  pmtrfv  19393  pmtrmvd  19397  pmtrfb  19406  odmodnn0  19481  oddvdsnn0  19485  odnncl  19486  odmod  19487  oddvds  19488  odeq  19491  odmulgid  19495  odmulg  19497  odmulgeq  19498  odbezout  19499  odf1o1  19513  odf1o2  19514  odngen  19518  odcau  19545  pgpssslw  19555  fislw  19566  lsmless1x  19585  lsmless2x  19586  lsmsubm  19594  lsmmod  19616  lsmmod2  19617  efgsfo  19680  cntzcmn  19781  odadd1  19789  odadd2  19790  odadd  19791  lsmcomx  19797  prdscmnd  19802  gsumconst  19875  ring1eq0  20245  cntzsubrng  20512  cntzsubr  20551  isabvd  20757  rmodislmod  20893  lspss  20947  0lmhm  21004  reslmhm2  21017  pwssplit0  21022  pwssplit1  21023  lbspss  21046  lspfixed  21095  lsmcv  21108  lspsnat  21112  2idlcpblrng  21238  cnfldfunALT  21336  cnfldfunALTOLD  21349  xrsdsreclblem  21379  obselocv  21695  frlmsplit2  21740  frlmsslss2  21742  frlmup4  21768  lindff1  21787  lsslindf  21797  lsslinds  21798  islindf4  21805  issubassa  21834  aspss  21844  coe1subfv  22220  coe1tm  22227  mpomatmul  22402  mamutpos  22414  submaval  22537  mdetdiag  22555  mdetunilem1  22568  mdetunilem3  22570  mdetunilem9  22576  mdetmul  22579  maducoeval2  22596  madurid  22600  minmar1val  22604  cramer  22647  cpmatel2  22669  m2cpm  22697  decpmatmul  22728  pmatcollpw1lem2  22731  pmatcollpw1  22732  pmatcollpw2lem  22733  pm2mpcl  22753  mply1topmatcl  22761  mp2pm2mplem2  22763  mp2pm2mplem4  22765  pm2mpghmlem2  22768  pm2mpghmlem1  22769  cayhamlem2  22840  neiint  23060  topssnei  23080  cnrest2  23242  cnprest2  23246  cnt0  23302  cnt1  23306  cnhaus  23310  cncmp  23348  fiuncmp  23360  sscmp  23361  hauscmp  23363  cnconn  23378  unconn  23385  comppfsc  23488  kgen2ss  23511  ptpjopn  23568  ptrescn  23595  qtopss  23671  kqfvima  23686  r0cld  23694  cmphaushmeo  23756  fbssint  23794  fbasrn  23840  filuni  23841  ufilmax  23863  fin1aufil  23888  fmf  23901  fmss  23902  rnelfmlem  23908  rnelfm  23909  fmufil  23915  fmco  23917  flimss2  23928  flimss1  23929  flimrest  23939  cnpflf2  23956  cnpflf  23957  flfcnp  23960  lmflf  23961  supnfcls  23976  fclsss1  23978  fclsss2  23979  cnpfcfi  23996  subgntr  24063  opnsubg  24064  cldsubg  24067  ustuqtop1  24197  ucncn  24240  bldisj  24354  blgt0  24355  bl2in  24356  blss2ps  24359  blss2  24360  xbln0  24370  blssps  24380  blss  24381  lpbl  24459  blcld  24461  blcls  24462  stdbdmopn  24474  metcnp2  24498  txmetcnp  24503  blval2  24518  restmetu  24526  nmoix  24685  nmoi2  24686  nmoeq0  24692  nmotri  24695  metdsge  24806  metds0  24807  metdseq0  24811  icoopnst  24904  iccpnfhmeo  24911  xrhmeo  24912  nmhmcn  25088  cphsqrtcl2  25154  cphsqrtcl3  25155  fmcfil  25240  bcthlem5  25296  cmetcusp1  25321  cssbn  25343  pjth  25407  ovolunnul  25469  volun  25514  voliunlem2  25520  itg2const  25709  iblconst  25787  itgconst  25788  limcvallem  25840  dvcnp2  25889  dvcnp2OLD  25890  dvcn  25891  deg1mul3le  26090  deg1tmle  26091  idomrootle  26146  ig1pdvds  26153  coe11  26226  dgrmulc  26245  dvply1  26259  aaliou2  26316  efcvx  26427  tanord  26515  logdivlti  26597  logccv  26640  recxpcl  26652  cxplea  26673  cxple2a  26676  ang180  26792  isosctrlem2  26797  cxp2lim  26955  amgm  26969  muval1  27111  dvdssqf  27116  mumullem2  27158  bcmono  27256  lgsneg  27300  lgsmod  27302  lgsdirprm  27310  lgsdir  27311  lgsdi  27313  ltsres  27642  nolt02olem  27674  nolt02o  27675  nogt01o  27676  nosupbnd1lem1  27688  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd1lem6  27693  noinfbnd1lem1  27703  noinfbnd1lem4  27706  noinfbnd1lem6  27708  noinfbnd2  27711  noetainflem3  27719  ltslpss  27916  cofslts  27926  coinitslts  27927  cofcutrtime  27935  addsass  28013  addsdi  28163  mulsass  28174  ltmuls2  28179  norecdiv  28198  z12bdaylem  28492  brbtwn2  28990  colinearalglem1  28991  colinearalg  28995  axcgrtr  29000  axcontlem2  29050  upgrewlkle2  29692  wlksoneq1eq2  29748  crctcshwlkn0lem5  29899  wspthsnwspthsnon  30001  lppthon  30238  upgriseupth  30294  4cyclusnfrgr  30379  numclwwlk1lem2foa  30441  numclwwlk5  30475  nvmul0or  30737  shless  31446  shlej1  31447  pjspansn  31664  kbmul  32042  homco2  32064  kbass2  32204  fnpreimac  32759  padct  32807  eliccelico  32867  elicoelioo  32868  iocinioc2  32869  difioo  32872  nexple  32935  swrdrn2  33046  swrdrn3  33047  xrge0npcan  33112  isarchi2  33278  archiabl  33291  pidlnz  33468  lindssn  33470  ssmxidl  33566  mdetlap1  34003  zarclsiin  34048  pstmfval  34073  fmcncfil  34108  zrhnm  34144  qqhnm  34167  volfiniune  34407  omsmeas  34500  eulerpartlemb  34545  probinc  34598  cndprob01  34612  signswmnd  34734  cvmsss2  35487  funsseq  35981  cgrtriv  36215  5segofs  36219  btwntriv2  36225  btwnxfr  36269  segcon2  36318  brsegle2  36322  seglelin  36329  outsideofeu  36344  weiunpo  36678  weiunfr  36680  weiunse  36681  lindsenlbs  37860  mblfinlem2  37903  blbnd  38032  rrndstprj2  38076  zerdivemp1x  38192  lsmsat  39378  lsatfixedN  39379  lssat  39386  lkrlsp  39472  lshpkrlem4  39483  cvrcon3b  39647  leat3  39665  atlen0  39680  atnle  39687  atlatmstc  39689  atlatle  39690  cvlcvr1  39709  cvlsupr2  39713  hlsupr2  39757  hlrelat2  39773  cvrexchlem  39789  cvratlem  39791  lnnat  39797  atexchcvrN  39810  1cvratlt  39844  1cvrjat  39845  3atlem3  39855  3atlem7  39859  llni2  39882  atcvrlln2  39889  llnexatN  39891  llncmp  39892  2llnmat  39894  2at0mat0  39895  2atnelpln  39914  llncvrlpln2  39927  2lplnmN  39929  2llnmj  39930  lplncmp  39932  lplnexatN  39933  2llnjaN  39936  lvoli3  39947  islvol2aN  39962  4atlem3a  39967  4atlem4a  39969  4atlem4b  39970  4atlem11  39979  4atlem12  39982  lplncvrlvol2  39985  lvolcmp  39987  2lplnmj  39992  islinei  40110  linepmap  40145  lneq2at  40148  2llnma3r  40158  elpaddn0  40170  elpaddatriN  40173  elpaddat  40174  paddcom  40183  paddss1  40187  paddss2  40188  paddasslem6  40195  paddasslem7  40196  paddasslem10  40199  paddasslem15  40204  pmodlem2  40217  pmodl42N  40221  pmapjoin  40222  atmod1i1m  40228  llnmod1i2  40230  llnexchb2lem  40238  polcon2bN  40290  pclfinclN  40320  poml4N  40323  poml6N  40325  osumcllem11N  40336  osumclN  40337  pmapojoinN  40338  pexmidlem2N  40341  pexmidlem3N  40342  pexmidlem4N  40343  pexmidlem6N  40345  pexmidlem7N  40346  pl42lem2N  40350  pl42lem3N  40351  pl42lem4N  40352  pl42N  40353  lhpexle3lem  40381  lhpmcvr3  40395  lhp2at0nle  40405  lhprelat3N  40410  lauteq  40465  lautco  40467  ltrncoidN  40498  ltrneq2  40518  ltrnnidn  40544  ltrnideq  40545  trlnle  40556  cdlemc  40567  cdlemd4  40571  cdlemd5  40572  cdlemd9  40576  cdlemd  40577  ltrneq3  40578  cdlemefrs29pre00  40765  cdlemefrs29cpre1  40768  cdlemefrs29clN  40769  cdlemefrs32fva  40770  cdlemefr29exN  40772  cdlemefr27cl  40773  cdlemefs27cl  40783  cdlemefs32sn1aw  40784  cdleme32fva  40807  cdleme32d  40814  cdleme32f  40816  cdleme32le  40817  cdleme40n  40838  cdleme41snaw  40846  cdleme17d3  40866  cdleme48fvg  40870  cdlemeg46fvcl  40876  cdlemeg46fgN  40904  cdleme48fgv  40908  ltrniotavalbN  40954  cdlemb3  40976  cdlemg15  41026  cdlemg17dN  41033  trlco  41097  cdlemg44b  41102  ltrncom  41108  trljco  41110  tendococl  41142  tendoplcl  41151  tendoplcom  41152  tendotr  41200  cdlemk36  41283  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk19x  41313  cdlemk53b  41326  cdlemk55  41331  cdlemk35u  41334  cdlemk55u  41336  cdlemk39u  41338  cdlemk19u  41340  cdlemk56  41341  tendoex  41345  cdleml5N  41350  dihord2pre  41595  dihord6apre  41626  dihord5b  41629  dihord5apre  41632  dihord  41634  dihmeetlem1N  41660  dihmeetlem2N  41669  dihglbcpreN  41670  dihmeetbN  41673  dihmeetlem4preN  41676  dihmeetlem5  41678  dihmeetlem6  41679  dihmeetlem7N  41680  dihmeetlem10N  41686  dihmeetlem11N  41687  dihmeetlem12N  41688  dihmeetlem13N  41689  dihmeetlem15N  41691  dihmeetlem17N  41693  dihmeetlem18N  41694  dihmeetlem19N  41695  dihmeetALTN  41697  dih1dimatlem0  41698  dihlspsnssN  41702  dvh3dim2  41818  sticksstones1  42510  sticksstones2  42511  sticksstones12  42522  aks6d1c6isolem1  42538  dvdsexpnn  42697  resubcan2  42752  mzpsubst  43099  diophrw  43110  eldioph2lem1  43111  rencldnfi  43172  pellexlem2  43181  pellqrexplicit  43228  infmrgelbi  43229  rmxycomplete  43268  congadd  43317  acongeq  43334  jm2.19  43344  jm2.22  43346  jm2.20nn  43348  jm2.25lem1  43349  jm2.27  43359  jm3.1  43371  lmhmlnmsplit  43438  pwssplit4  43440  hbtlem2  43475  dgraa0p  43500  proot1hash  43546  iocunico  43562  cantnf2  43676  dflim5  43680  omcl2  43684  tfsconcatrn  43693  nadd2rabex  43737  relexpxpmin  44067  brtrclfv2  44077  ntrclsk3  44420  grur1cld  44582  ismnu  44611  suprnmpt  45527  wessf1ornlem  45538  choicefi  45552  supxrgere  45686  supxrgelem  45690  supxrge  45691  infleinflem2  45723  snunioo1  45866  iccintsng  45877  fmul01  45934  lptre2pt  45992  0ellimcdiv  46001  fnlimfvre  46026  limsupmnfuzlem  46078  climisp  46098  limsupgtlem  46129  ibliccsinexp  46303  iblioosinexp  46305  volioc  46324  iblspltprt  46325  stoweidlem20  46372  stoweidlem22  46374  stoweidlem34  46386  stoweidlem44  46396  stoweidlem60  46412  wallispilem3  46419  fourierdlem42  46501  fourierdlem51  46509  fourierdlem54  46512  fourierdlem87  46545  fourierdlem97  46555  ioorrnopnlem  46656  sge0seq  46798  hoicvr  46900  fsupdm  47194  finfdm  47198  3f1oss1  47429  funfocofob  47432  imasetpreimafvbijlemfv  47756  uhgrimisgrgric  48285  uhgrimgrlim  48341  fprmappr  48699  lincresunit3lem3  48828  lindssnlvec  48840  rrx2linesl  49097  line2  49106  itsclc0lem3  49112  itsclc0yqsollem1  49116  itscnhlc0xyqsol  49119  itschlc0xyqsol1  49120  itsclc0  49125  itscnhlinecirc02plem2  49137  itscnhlinecirc02plem3  49138  uptrlem1  49563  uptr2  49574  setc1onsubc  49955