Theorem simpl3 1193

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 1187	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  1250  simpl23  1253  simpl33  1256  simp1l3  1268  simp2l3  1274  simp3l3  1280  3anandirs  1472  2nreu  4467  predtrss  6354  frpomin  6372  f1prex  7320  fcofo  7324  soisores  7363  weniso  7390  knatar  7393  ofmpteq  7736  funelss  8088  frrlem10  8336  fprlem1  8341  smocdmdom  8424  nnmord  8688  nnmword  8689  naddasslem1  8750  naddasslem2  8751  difsnen  9119  mapunen  9212  ac6sfi  9348  fipreima  9428  wemaplem2  9616  wemapso2lem  9621  ttrclselem2  9795  en2eqpr  10076  indcardi  10110  acndom  10120  fodomfi2  10129  infmap2  10286  cflim2  10332  coftr  10342  infpssrlem4  10375  fin23lem11  10386  fincssdom  10392  isf32lem9  10430  fin1a2lem9  10477  gchpwdom  10739  gruima  10871  prpssnq  11059  distrlem4pr  11095  dedekind  11453  addcan  11474  addcan2  11475  divmulass  11972  supmul1  12264  uzsupss  13005  xaddass  13311  xleadd1a  13315  xlesubadd  13325  xmulasslem3  13348  xmulass  13349  xadddilem  13356  xadddi  13357  ixxun  13423  icoshftf1o  13534  snunioc  13540  difelfzle  13698  fzo1fzo0n0  13767  ssfzoulel  13810  modmuladd  13964  modifeq2int  13984  modaddmulmod  13989  modsubdir  13991  ltexp2a  14216  leexp2  14221  ltexp2r  14223  exple1  14226  expnlbnd2  14283  mulsubdivbinom2  14311  hashtpg  14534  ccatass  14636  ccatopth  14764  pfxccatin12lem2a  14775  pfxccat3  14782  cshinj  14859  2cshw  14861  s2f1o  14965  limsupgre  15527  addcn2  15640  mulcn2  15642  binomrisefac  16090  bpolydif  16103  dvdsmodexp  16310  modmulconst  16336  dvdsexp2im  16375  dvdsmod  16377  sadass  16517  gcdass  16594  rplpwr  16605  rpmulgcd2  16703  rpdvds  16707  rpexp  16769  prmdiveq  16833  hashgcdlem  16835  coprimeprodsq  16855  coprimeprodsq2  16856  pythagtriplem3  16865  pcdvdsb  16916  pcgcd1  16924  dvdsprmpweq  16931  pcbc  16947  0ram  17067  ramz2  17071  ramub1lem1  17073  mremre  17662  mrieqv2d  17697  lubun  18585  isnsgrp  18761  issubmnd  18799  frmdss2  18898  submefmnd  18930  sgrp2rid2ex  18962  mulgnn0p1  19125  mulgnnsubcl  19126  mulgneg  19132  mulgdirlem  19145  nmzsubg  19205  ghmmulg  19268  pmtrfv  19494  pmtrmvd  19498  pmtrfb  19507  odmodnn0  19582  oddvdsnn0  19586  odnncl  19587  odmod  19588  oddvds  19589  odeq  19592  odmulgid  19596  odmulg  19598  odmulgeq  19599  odbezout  19600  odf1o1  19614  odf1o2  19615  odngen  19619  odcau  19646  pgpssslw  19656  fislw  19667  lsmless1x  19686  lsmless2x  19687  lsmsubm  19695  lsmmod  19717  lsmmod2  19718  efgsfo  19781  cntzcmn  19882  odadd1  19890  odadd2  19891  odadd  19892  lsmcomx  19898  prdscmnd  19903  gsumconst  19976  ring1eq0  20321  cntzsubrng  20593  cntzsubr  20634  isabvd  20835  rmodislmod  20950  rmodislmodOLD  20951  lspss  21005  0lmhm  21062  reslmhm2  21075  pwssplit0  21080  pwssplit1  21081  lbspss  21104  lspfixed  21153  lsmcv  21166  lspsnat  21170  2idlcpblrng  21304  cnfldfunALT  21402  cnfldfunALTOLD  21415  xrsdsreclblem  21453  obselocv  21771  frlmsplit2  21816  frlmsslss2  21818  frlmup4  21844  lindff1  21863  lsslindf  21873  lsslinds  21874  islindf4  21881  issubassa  21910  aspss  21920  coe1subfv  22290  coe1tm  22297  mpomatmul  22473  mamutpos  22485  submaval  22608  mdetdiag  22626  mdetunilem1  22639  mdetunilem3  22641  mdetunilem9  22647  mdetmul  22650  maducoeval2  22667  madurid  22671  minmar1val  22675  cramer  22718  cpmatel2  22740  m2cpm  22768  decpmatmul  22799  pmatcollpw1lem2  22802  pmatcollpw1  22803  pmatcollpw2lem  22804  pm2mpcl  22824  mply1topmatcl  22832  mp2pm2mplem2  22834  mp2pm2mplem4  22836  pm2mpghmlem2  22839  pm2mpghmlem1  22840  cayhamlem2  22911  neiint  23133  topssnei  23153  cnrest2  23315  cnprest2  23319  cnt0  23375  cnt1  23379  cnhaus  23383  cncmp  23421  fiuncmp  23433  sscmp  23434  hauscmp  23436  cnconn  23451  unconn  23458  comppfsc  23561  kgen2ss  23584  ptpjopn  23641  ptrescn  23668  qtopss  23744  kqfvima  23759  r0cld  23767  cmphaushmeo  23829  fbssint  23867  fbasrn  23913  filuni  23914  ufilmax  23936  fin1aufil  23961  fmf  23974  fmss  23975  rnelfmlem  23981  rnelfm  23982  fmufil  23988  fmco  23990  flimss2  24001  flimss1  24002  flimrest  24012  cnpflf2  24029  cnpflf  24030  flfcnp  24033  lmflf  24034  supnfcls  24049  fclsss1  24051  fclsss2  24052  cnpfcfi  24069  subgntr  24136  opnsubg  24137  cldsubg  24140  ustuqtop1  24271  ucncn  24315  bldisj  24429  blgt0  24430  bl2in  24431  blss2ps  24434  blss2  24435  xbln0  24445  blssps  24455  blss  24456  lpbl  24537  blcld  24539  blcls  24540  stdbdmopn  24552  metcnp2  24576  txmetcnp  24581  blval2  24596  restmetu  24604  nmoix  24771  nmoi2  24772  nmoeq0  24778  nmotri  24781  metdsge  24890  metds0  24891  metdseq0  24895  icoopnst  24988  iccpnfhmeo  24995  xrhmeo  24996  nmhmcn  25172  cphsqrtcl2  25239  cphsqrtcl3  25240  fmcfil  25325  bcthlem5  25381  cmetcusp1  25406  cssbn  25428  pjth  25492  ovolunnul  25554  volun  25599  voliunlem2  25605  itg2const  25795  iblconst  25873  itgconst  25874  limcvallem  25926  dvcnp2  25975  dvcnp2OLD  25976  dvcn  25977  deg1mul3le  26176  deg1tmle  26177  idomrootle  26232  ig1pdvds  26239  coe11  26312  dgrmulc  26331  dvply1  26343  aaliou2  26400  efcvx  26511  tanord  26598  logdivlti  26680  logccv  26723  recxpcl  26735  cxplea  26756  cxple2a  26759  ang180  26875  isosctrlem2  26880  cxp2lim  27038  amgm  27052  muval1  27194  dvdssqf  27199  mumullem2  27241  bcmono  27339  lgsneg  27383  lgsmod  27385  lgsdirprm  27393  lgsdir  27394  lgsdi  27396  sltres  27725  nolt02olem  27757  nolt02o  27758  nogt01o  27759  nosupbnd1lem1  27771  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  noinfbnd1lem1  27786  noinfbnd1lem4  27789  noinfbnd1lem6  27791  noinfbnd2  27794  noetainflem3  27802  sltlpss  27963  cofsslt  27970  coinitsslt  27971  cofcutrtime  27979  addsass  28056  addsdi  28199  mulsass  28210  sltmul2  28215  norecdiv  28234  brbtwn2  28938  colinearalglem1  28939  colinearalg  28943  axcgrtr  28948  axcontlem2  28998  upgrewlkle2  29642  wlksoneq1eq2  29700  crctcshwlkn0lem5  29847  wspthsnwspthsnon  29949  lppthon  30183  upgriseupth  30239  4cyclusnfrgr  30324  numclwwlk1lem2foa  30386  numclwwlk5  30420  nvmul0or  30682  shless  31391  shlej1  31392  pjspansn  31609  kbmul  31987  homco2  32009  kbass2  32149  fnpreimac  32689  padct  32733  eliccelico  32782  elicoelioo  32783  iocinioc2  32784  difioo  32787  swrdrn2  32921  swrdrn3  32922  xrge0npcan  33006  isarchi2  33165  archiabl  33178  pidlnz  33369  lindssn  33371  ssmxidl  33467  mdetlap1  33772  zarclsiin  33817  pstmfval  33842  fmcncfil  33877  zrhnm  33915  qqhnm  33936  nexple  33973  volfiniune  34194  omsmeas  34288  eulerpartlemb  34333  probinc  34386  cndprob01  34400  signswmnd  34534  cvmsss2  35242  funsseq  35731  cgrtriv  35966  5segofs  35970  btwntriv2  35976  btwnxfr  36020  segcon2  36069  brsegle2  36073  seglelin  36080  outsideofeu  36095  weiunpo  36431  weiunfr  36433  weiunse  36434  lindsenlbs  37575  mblfinlem2  37618  blbnd  37747  rrndstprj2  37791  zerdivemp1x  37907  lsmsat  38964  lsatfixedN  38965  lssat  38972  lkrlsp  39058  lshpkrlem4  39069  cvrcon3b  39233  leat3  39251  atlen0  39266  atnle  39273  atlatmstc  39275  atlatle  39276  cvlcvr1  39295  cvlsupr2  39299  hlsupr2  39344  hlrelat2  39360  cvrexchlem  39376  cvratlem  39378  lnnat  39384  atexchcvrN  39397  1cvratlt  39431  1cvrjat  39432  3atlem3  39442  3atlem7  39446  llni2  39469  atcvrlln2  39476  llnexatN  39478  llncmp  39479  2llnmat  39481  2at0mat0  39482  2atnelpln  39501  llncvrlpln2  39514  2lplnmN  39516  2llnmj  39517  lplncmp  39519  lplnexatN  39520  2llnjaN  39523  lvoli3  39534  islvol2aN  39549  4atlem3a  39554  4atlem4a  39556  4atlem4b  39557  4atlem11  39566  4atlem12  39569  lplncvrlvol2  39572  lvolcmp  39574  2lplnmj  39579  islinei  39697  linepmap  39732  lneq2at  39735  2llnma3r  39745  elpaddn0  39757  elpaddatriN  39760  elpaddat  39761  paddcom  39770  paddss1  39774  paddss2  39775  paddasslem6  39782  paddasslem7  39783  paddasslem10  39786  paddasslem15  39791  pmodlem2  39804  pmodl42N  39808  pmapjoin  39809  atmod1i1m  39815  llnmod1i2  39817  llnexchb2lem  39825  polcon2bN  39877  pclfinclN  39907  poml4N  39910  poml6N  39912  osumcllem11N  39923  osumclN  39924  pmapojoinN  39925  pexmidlem2N  39928  pexmidlem3N  39929  pexmidlem4N  39930  pexmidlem6N  39932  pexmidlem7N  39933  pl42lem2N  39937  pl42lem3N  39938  pl42lem4N  39939  pl42N  39940  lhpexle3lem  39968  lhpmcvr3  39982  lhp2at0nle  39992  lhprelat3N  39997  lauteq  40052  lautco  40054  ltrncoidN  40085  ltrneq2  40105  ltrnnidn  40131  ltrnideq  40132  trlnle  40143  cdlemc  40154  cdlemd4  40158  cdlemd5  40159  cdlemd9  40163  cdlemd  40164  ltrneq3  40165  cdlemefrs29pre00  40352  cdlemefrs29cpre1  40355  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdlemefr29exN  40359  cdlemefr27cl  40360  cdlemefs27cl  40370  cdlemefs32sn1aw  40371  cdleme32fva  40394  cdleme32d  40401  cdleme32f  40403  cdleme32le  40404  cdleme40n  40425  cdleme41snaw  40433  cdleme17d3  40453  cdleme48fvg  40457  cdlemeg46fvcl  40463  cdlemeg46fgN  40491  cdleme48fgv  40495  ltrniotavalbN  40541  cdlemb3  40563  cdlemg15  40613  cdlemg17dN  40620  trlco  40684  cdlemg44b  40689  ltrncom  40695  trljco  40697  tendococl  40729  tendoplcl  40738  tendoplcom  40739  tendotr  40787  cdlemk36  40870  cdlemk35s-id  40895  cdlemk39s-id  40897  cdlemk19x  40900  cdlemk53b  40913  cdlemk55  40918  cdlemk35u  40921  cdlemk55u  40923  cdlemk39u  40925  cdlemk19u  40927  cdlemk56  40928  tendoex  40932  cdleml5N  40937  dihord2pre  41182  dihord6apre  41213  dihord5b  41216  dihord5apre  41219  dihord  41221  dihmeetlem1N  41247  dihmeetlem2N  41256  dihglbcpreN  41257  dihmeetbN  41260  dihmeetlem4preN  41263  dihmeetlem5  41265  dihmeetlem6  41266  dihmeetlem7N  41267  dihmeetlem10N  41273  dihmeetlem11N  41274  dihmeetlem12N  41275  dihmeetlem13N  41276  dihmeetlem15N  41278  dihmeetlem17N  41280  dihmeetlem18N  41281  dihmeetlem19N  41282  dihmeetALTN  41284  dih1dimatlem0  41285  dihlspsnssN  41289  dvh3dim2  41405  sticksstones1  42103  sticksstones2  42104  sticksstones12  42115  aks6d1c6isolem1  42131  dvdsexpnn  42320  resubcan2  42364  mzpsubst  42704  diophrw  42715  eldioph2lem1  42716  rencldnfi  42777  pellexlem2  42786  pellqrexplicit  42833  infmrgelbi  42834  rmxycomplete  42874  congadd  42923  acongeq  42940  jm2.19  42950  jm2.22  42952  jm2.20nn  42954  jm2.25lem1  42955  jm2.27  42965  jm3.1  42977  lmhmlnmsplit  43044  pwssplit4  43046  hbtlem2  43081  dgraa0p  43106  proot1hash  43156  iocunico  43172  cantnf2  43287  dflim5  43291  omcl2  43295  tfsconcatrn  43304  nadd2rabex  43348  relexpxpmin  43679  brtrclfv2  43689  ntrclsk3  44032  grur1cld  44201  ismnu  44230  suprnmpt  45081  wessf1ornlem  45092  choicefi  45107  supxrgere  45248  supxrgelem  45252  supxrge  45253  infleinflem2  45286  snunioo1  45430  iccintsng  45441  fmul01  45501  lptre2pt  45561  0ellimcdiv  45570  fnlimfvre  45595  limsupmnfuzlem  45647  climisp  45667  limsupgtlem  45698  ibliccsinexp  45872  iblioosinexp  45874  volioc  45893  iblspltprt  45894  stoweidlem20  45941  stoweidlem22  45943  stoweidlem34  45955  stoweidlem44  45965  stoweidlem60  45981  wallispilem3  45988  fourierdlem42  46070  fourierdlem51  46078  fourierdlem54  46081  fourierdlem87  46114  fourierdlem97  46124  ioorrnopnlem  46225  sge0seq  46367  hoicvr  46469  fsupdm  46763  finfdm  46767  3f1oss1  46990  funfocofob  46993  imasetpreimafvbijlemfv  47276  uhgrimisgrgric  47783  uhgrimgrlim  47811  fprmappr  48070  lincresunit3lem3  48203  lindssnlvec  48215  rrx2linesl  48477  line2  48486  itsclc0lem3  48492  itsclc0yqsollem1  48496  itscnhlc0xyqsol  48499  itschlc0xyqsol1  48500  itsclc0  48505  itscnhlinecirc02plem2  48517  itscnhlinecirc02plem3  48518