Theorem simpl3 1194

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 1188	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  simpl13  1251  simpl23  1254  simpl33  1257  simp1l3  1269  simp2l3  1275  simp3l3  1281  3anandirs  1474  2nreu  4393  predtrss  6274  frpomin  6292  f1prex  7224  fcofo  7228  soisores  7267  weniso  7294  knatar  7297  ofmpteq  7639  funelss  7985  frrlem10  8231  fprlem1  8236  smocdmdom  8294  nnmord  8553  nnmword  8554  naddasslem1  8615  naddasslem2  8616  difsnen  8979  mapunen  9066  ac6sfi  9175  fipreima  9249  wemaplem2  9440  wemapso2lem  9445  ttrclselem2  9623  en2eqpr  9905  indcardi  9939  acndom  9949  fodomfi2  9958  infmap2  10115  cflim2  10161  coftr  10171  infpssrlem4  10204  fin23lem11  10215  fincssdom  10221  isf32lem9  10259  fin1a2lem9  10306  gchpwdom  10568  gruima  10700  prpssnq  10888  distrlem4pr  10924  dedekind  11283  addcan  11304  addcan2  11305  divmulass  11806  supmul1  12098  uzsupss  12840  xaddass  13150  xleadd1a  13154  xlesubadd  13164  xmulasslem3  13187  xmulass  13188  xadddilem  13195  xadddi  13196  ixxun  13263  icoshftf1o  13376  snunioc  13382  difelfzle  13543  fzo1fzo0n0  13617  ssfzoulel  13662  modmuladd  13822  modifeq2int  13842  modaddmulmod  13847  modsubdir  13849  ltexp2a  14075  leexp2  14080  ltexp2r  14082  exple1  14086  expnlbnd2  14143  mulsubdivbinom2  14171  hashtpg  14394  ccatass  14498  ccatopth  14625  pfxccatin12lem2a  14636  pfxccat3  14643  cshinj  14720  2cshw  14722  s2f1o  14825  limsupgre  15390  addcn2  15503  mulcn2  15505  binomrisefac  15951  bpolydif  15964  dvdsmodexp  16173  modmulconst  16201  dvdsexp2im  16240  dvdsmod  16242  sadass  16384  gcdass  16460  rplpwr  16471  rpmulgcd2  16569  rpdvds  16573  rpexp  16635  prmdiveq  16699  hashgcdlem  16701  coprimeprodsq  16722  coprimeprodsq2  16723  pythagtriplem3  16732  pcdvdsb  16783  pcgcd1  16791  dvdsprmpweq  16798  pcbc  16814  0ram  16934  ramz2  16938  ramub1lem1  16940  mremre  17508  mrieqv2d  17547  lubun  18423  isnsgrp  18633  issubmnd  18671  frmdss2  18773  submefmnd  18805  sgrp2rid2ex  18837  mulgnn0p1  19000  mulgnnsubcl  19001  mulgneg  19007  mulgdirlem  19020  nmzsubg  19079  ghmmulg  19142  pmtrfv  19366  pmtrmvd  19370  pmtrfb  19379  odmodnn0  19454  oddvdsnn0  19458  odnncl  19459  odmod  19460  oddvds  19461  odeq  19464  odmulgid  19468  odmulg  19470  odmulgeq  19471  odbezout  19472  odf1o1  19486  odf1o2  19487  odngen  19491  odcau  19518  pgpssslw  19528  fislw  19539  lsmless1x  19558  lsmless2x  19559  lsmsubm  19567  lsmmod  19589  lsmmod2  19590  efgsfo  19653  cntzcmn  19754  odadd1  19762  odadd2  19763  odadd  19764  lsmcomx  19770  prdscmnd  19775  gsumconst  19848  ring1eq0  20218  cntzsubrng  20484  cntzsubr  20523  isabvd  20729  rmodislmod  20865  lspss  20919  0lmhm  20976  reslmhm2  20989  pwssplit0  20994  pwssplit1  20995  lbspss  21018  lspfixed  21067  lsmcv  21080  lspsnat  21084  2idlcpblrng  21210  cnfldfunALT  21308  cnfldfunALTOLD  21321  xrsdsreclblem  21351  obselocv  21667  frlmsplit2  21712  frlmsslss2  21714  frlmup4  21740  lindff1  21759  lsslindf  21769  lsslinds  21770  islindf4  21777  issubassa  21806  aspss  21816  coe1subfv  22181  coe1tm  22188  mpomatmul  22362  mamutpos  22374  submaval  22497  mdetdiag  22515  mdetunilem1  22528  mdetunilem3  22530  mdetunilem9  22536  mdetmul  22539  maducoeval2  22556  madurid  22560  minmar1val  22564  cramer  22607  cpmatel2  22629  m2cpm  22657  decpmatmul  22688  pmatcollpw1lem2  22691  pmatcollpw1  22692  pmatcollpw2lem  22693  pm2mpcl  22713  mply1topmatcl  22721  mp2pm2mplem2  22723  mp2pm2mplem4  22725  pm2mpghmlem2  22728  pm2mpghmlem1  22729  cayhamlem2  22800  neiint  23020  topssnei  23040  cnrest2  23202  cnprest2  23206  cnt0  23262  cnt1  23266  cnhaus  23270  cncmp  23308  fiuncmp  23320  sscmp  23321  hauscmp  23323  cnconn  23338  unconn  23345  comppfsc  23448  kgen2ss  23471  ptpjopn  23528  ptrescn  23555  qtopss  23631  kqfvima  23646  r0cld  23654  cmphaushmeo  23716  fbssint  23754  fbasrn  23800  filuni  23801  ufilmax  23823  fin1aufil  23848  fmf  23861  fmss  23862  rnelfmlem  23868  rnelfm  23869  fmufil  23875  fmco  23877  flimss2  23888  flimss1  23889  flimrest  23899  cnpflf2  23916  cnpflf  23917  flfcnp  23920  lmflf  23921  supnfcls  23936  fclsss1  23938  fclsss2  23939  cnpfcfi  23956  subgntr  24023  opnsubg  24024  cldsubg  24027  ustuqtop1  24157  ucncn  24200  bldisj  24314  blgt0  24315  bl2in  24316  blss2ps  24319  blss2  24320  xbln0  24330  blssps  24340  blss  24341  lpbl  24419  blcld  24421  blcls  24422  stdbdmopn  24434  metcnp2  24458  txmetcnp  24463  blval2  24478  restmetu  24486  nmoix  24645  nmoi2  24646  nmoeq0  24652  nmotri  24655  metdsge  24766  metds0  24767  metdseq0  24771  icoopnst  24864  iccpnfhmeo  24871  xrhmeo  24872  nmhmcn  25048  cphsqrtcl2  25114  cphsqrtcl3  25115  fmcfil  25200  bcthlem5  25256  cmetcusp1  25281  cssbn  25303  pjth  25367  ovolunnul  25429  volun  25474  voliunlem2  25480  itg2const  25669  iblconst  25747  itgconst  25748  limcvallem  25800  dvcnp2  25849  dvcnp2OLD  25850  dvcn  25851  deg1mul3le  26050  deg1tmle  26051  idomrootle  26106  ig1pdvds  26113  coe11  26186  dgrmulc  26205  dvply1  26219  aaliou2  26276  efcvx  26387  tanord  26475  logdivlti  26557  logccv  26600  recxpcl  26612  cxplea  26633  cxple2a  26636  ang180  26752  isosctrlem2  26757  cxp2lim  26915  amgm  26929  muval1  27071  dvdssqf  27076  mumullem2  27118  bcmono  27216  lgsneg  27260  lgsmod  27262  lgsdirprm  27270  lgsdir  27271  lgsdi  27273  sltres  27602  nolt02olem  27634  nolt02o  27635  nogt01o  27636  nosupbnd1lem1  27648  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd1lem6  27653  noinfbnd1lem1  27663  noinfbnd1lem4  27666  noinfbnd1lem6  27668  noinfbnd2  27671  noetainflem3  27679  sltlpss  27854  cofsslt  27863  coinitsslt  27864  cofcutrtime  27872  addsass  27949  addsdi  28095  mulsass  28106  sltmul2  28111  norecdiv  28130  brbtwn2  28885  colinearalglem1  28886  colinearalg  28890  axcgrtr  28895  axcontlem2  28945  upgrewlkle2  29587  wlksoneq1eq2  29643  crctcshwlkn0lem5  29794  wspthsnwspthsnon  29896  lppthon  30133  upgriseupth  30189  4cyclusnfrgr  30274  numclwwlk1lem2foa  30336  numclwwlk5  30370  nvmul0or  30632  shless  31341  shlej1  31342  pjspansn  31559  kbmul  31937  homco2  31959  kbass2  32099  fnpreimac  32655  padct  32705  eliccelico  32764  elicoelioo  32765  iocinioc2  32766  difioo  32769  nexple  32832  swrdrn2  32942  swrdrn3  32943  xrge0npcan  33008  isarchi2  33161  archiabl  33174  pidlnz  33348  lindssn  33350  ssmxidl  33446  mdetlap1  33860  zarclsiin  33905  pstmfval  33930  fmcncfil  33965  zrhnm  34001  qqhnm  34024  volfiniune  34264  omsmeas  34357  eulerpartlemb  34402  probinc  34455  cndprob01  34469  signswmnd  34591  cvmsss2  35339  funsseq  35833  cgrtriv  36067  5segofs  36071  btwntriv2  36077  btwnxfr  36121  segcon2  36170  brsegle2  36174  seglelin  36181  outsideofeu  36196  weiunpo  36530  weiunfr  36532  weiunse  36533  lindsenlbs  37675  mblfinlem2  37718  blbnd  37847  rrndstprj2  37891  zerdivemp1x  38007  lsmsat  39127  lsatfixedN  39128  lssat  39135  lkrlsp  39221  lshpkrlem4  39232  cvrcon3b  39396  leat3  39414  atlen0  39429  atnle  39436  atlatmstc  39438  atlatle  39439  cvlcvr1  39458  cvlsupr2  39462  hlsupr2  39506  hlrelat2  39522  cvrexchlem  39538  cvratlem  39540  lnnat  39546  atexchcvrN  39559  1cvratlt  39593  1cvrjat  39594  3atlem3  39604  3atlem7  39608  llni2  39631  atcvrlln2  39638  llnexatN  39640  llncmp  39641  2llnmat  39643  2at0mat0  39644  2atnelpln  39663  llncvrlpln2  39676  2lplnmN  39678  2llnmj  39679  lplncmp  39681  lplnexatN  39682  2llnjaN  39685  lvoli3  39696  islvol2aN  39711  4atlem3a  39716  4atlem4a  39718  4atlem4b  39719  4atlem11  39728  4atlem12  39731  lplncvrlvol2  39734  lvolcmp  39736  2lplnmj  39741  islinei  39859  linepmap  39894  lneq2at  39897  2llnma3r  39907  elpaddn0  39919  elpaddatriN  39922  elpaddat  39923  paddcom  39932  paddss1  39936  paddss2  39937  paddasslem6  39944  paddasslem7  39945  paddasslem10  39948  paddasslem15  39953  pmodlem2  39966  pmodl42N  39970  pmapjoin  39971  atmod1i1m  39977  llnmod1i2  39979  llnexchb2lem  39987  polcon2bN  40039  pclfinclN  40069  poml4N  40072  poml6N  40074  osumcllem11N  40085  osumclN  40086  pmapojoinN  40087  pexmidlem2N  40090  pexmidlem3N  40091  pexmidlem4N  40092  pexmidlem6N  40094  pexmidlem7N  40095  pl42lem2N  40099  pl42lem3N  40100  pl42lem4N  40101  pl42N  40102  lhpexle3lem  40130  lhpmcvr3  40144  lhp2at0nle  40154  lhprelat3N  40159  lauteq  40214  lautco  40216  ltrncoidN  40247  ltrneq2  40267  ltrnnidn  40293  ltrnideq  40294  trlnle  40305  cdlemc  40316  cdlemd4  40320  cdlemd5  40321  cdlemd9  40325  cdlemd  40326  ltrneq3  40327  cdlemefrs29pre00  40514  cdlemefrs29cpre1  40517  cdlemefrs29clN  40518  cdlemefrs32fva  40519  cdlemefr29exN  40521  cdlemefr27cl  40522  cdlemefs27cl  40532  cdlemefs32sn1aw  40533  cdleme32fva  40556  cdleme32d  40563  cdleme32f  40565  cdleme32le  40566  cdleme40n  40587  cdleme41snaw  40595  cdleme17d3  40615  cdleme48fvg  40619  cdlemeg46fvcl  40625  cdlemeg46fgN  40653  cdleme48fgv  40657  ltrniotavalbN  40703  cdlemb3  40725  cdlemg15  40775  cdlemg17dN  40782  trlco  40846  cdlemg44b  40851  ltrncom  40857  trljco  40859  tendococl  40891  tendoplcl  40900  tendoplcom  40901  tendotr  40949  cdlemk36  41032  cdlemk35s-id  41057  cdlemk39s-id  41059  cdlemk19x  41062  cdlemk53b  41075  cdlemk55  41080  cdlemk35u  41083  cdlemk55u  41085  cdlemk39u  41087  cdlemk19u  41089  cdlemk56  41090  tendoex  41094  cdleml5N  41099  dihord2pre  41344  dihord6apre  41375  dihord5b  41378  dihord5apre  41381  dihord  41383  dihmeetlem1N  41409  dihmeetlem2N  41418  dihglbcpreN  41419  dihmeetbN  41422  dihmeetlem4preN  41425  dihmeetlem5  41427  dihmeetlem6  41428  dihmeetlem7N  41429  dihmeetlem10N  41435  dihmeetlem11N  41436  dihmeetlem12N  41437  dihmeetlem13N  41438  dihmeetlem15N  41440  dihmeetlem17N  41442  dihmeetlem18N  41443  dihmeetlem19N  41444  dihmeetALTN  41446  dih1dimatlem0  41447  dihlspsnssN  41451  dvh3dim2  41567  sticksstones1  42259  sticksstones2  42260  sticksstones12  42271  aks6d1c6isolem1  42287  dvdsexpnn  42451  resubcan2  42506  mzpsubst  42865  diophrw  42876  eldioph2lem1  42877  rencldnfi  42938  pellexlem2  42947  pellqrexplicit  42994  infmrgelbi  42995  rmxycomplete  43034  congadd  43083  acongeq  43100  jm2.19  43110  jm2.22  43112  jm2.20nn  43114  jm2.25lem1  43115  jm2.27  43125  jm3.1  43137  lmhmlnmsplit  43204  pwssplit4  43206  hbtlem2  43241  dgraa0p  43266  proot1hash  43312  iocunico  43328  cantnf2  43442  dflim5  43446  omcl2  43450  tfsconcatrn  43459  nadd2rabex  43503  relexpxpmin  43834  brtrclfv2  43844  ntrclsk3  44187  grur1cld  44349  ismnu  44378  suprnmpt  45295  wessf1ornlem  45306  choicefi  45321  supxrgere  45456  supxrgelem  45460  supxrge  45461  infleinflem2  45493  snunioo1  45636  iccintsng  45647  fmul01  45704  lptre2pt  45762  0ellimcdiv  45771  fnlimfvre  45796  limsupmnfuzlem  45848  climisp  45868  limsupgtlem  45899  ibliccsinexp  46073  iblioosinexp  46075  volioc  46094  iblspltprt  46095  stoweidlem20  46142  stoweidlem22  46144  stoweidlem34  46156  stoweidlem44  46166  stoweidlem60  46182  wallispilem3  46189  fourierdlem42  46271  fourierdlem51  46279  fourierdlem54  46282  fourierdlem87  46315  fourierdlem97  46325  ioorrnopnlem  46426  sge0seq  46568  hoicvr  46670  fsupdm  46964  finfdm  46968  3f1oss1  47199  funfocofob  47202  imasetpreimafvbijlemfv  47526  uhgrimisgrgric  48055  uhgrimgrlim  48111  fprmappr  48469  lincresunit3lem3  48599  lindssnlvec  48611  rrx2linesl  48868  line2  48877  itsclc0lem3  48883  itsclc0yqsollem1  48887  itscnhlc0xyqsol  48890  itschlc0xyqsol1  48891  itsclc0  48896  itscnhlinecirc02plem2  48908  itscnhlinecirc02plem3  48909  uptrlem1  49335  uptr2  49346  setc1onsubc  49727