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  4409  predtrss  6297  frpomin  6315  f1prex  7261  fcofo  7265  soisores  7304  weniso  7331  knatar  7334  ofmpteq  7678  funelss  8028  frrlem10  8276  fprlem1  8281  smocdmdom  8339  nnmord  8598  nnmword  8599  naddasslem1  8660  naddasslem2  8661  difsnen  9026  mapunen  9115  ac6sfi  9237  fipreima  9315  wemaplem2  9506  wemapso2lem  9511  ttrclselem2  9685  en2eqpr  9966  indcardi  10000  acndom  10010  fodomfi2  10019  infmap2  10176  cflim2  10222  coftr  10232  infpssrlem4  10265  fin23lem11  10276  fincssdom  10282  isf32lem9  10320  fin1a2lem9  10367  gchpwdom  10629  gruima  10761  prpssnq  10949  distrlem4pr  10985  dedekind  11343  addcan  11364  addcan2  11365  divmulass  11866  supmul1  12158  uzsupss  12905  xaddass  13215  xleadd1a  13219  xlesubadd  13229  xmulasslem3  13252  xmulass  13253  xadddilem  13260  xadddi  13261  ixxun  13328  icoshftf1o  13441  snunioc  13447  difelfzle  13608  fzo1fzo0n0  13682  ssfzoulel  13727  modmuladd  13884  modifeq2int  13904  modaddmulmod  13909  modsubdir  13911  ltexp2a  14137  leexp2  14142  ltexp2r  14144  exple1  14148  expnlbnd2  14205  mulsubdivbinom2  14233  hashtpg  14456  ccatass  14559  ccatopth  14687  pfxccatin12lem2a  14698  pfxccat3  14705  cshinj  14782  2cshw  14784  s2f1o  14888  limsupgre  15453  addcn2  15566  mulcn2  15568  binomrisefac  16014  bpolydif  16027  dvdsmodexp  16236  modmulconst  16264  dvdsexp2im  16303  dvdsmod  16305  sadass  16447  gcdass  16523  rplpwr  16534  rpmulgcd2  16632  rpdvds  16636  rpexp  16698  prmdiveq  16762  hashgcdlem  16764  coprimeprodsq  16785  coprimeprodsq2  16786  pythagtriplem3  16795  pcdvdsb  16846  pcgcd1  16854  dvdsprmpweq  16861  pcbc  16877  0ram  16997  ramz2  17001  ramub1lem1  17003  mremre  17571  mrieqv2d  17606  lubun  18480  isnsgrp  18656  issubmnd  18694  frmdss2  18796  submefmnd  18828  sgrp2rid2ex  18860  mulgnn0p1  19023  mulgnnsubcl  19024  mulgneg  19030  mulgdirlem  19043  nmzsubg  19103  ghmmulg  19166  pmtrfv  19388  pmtrmvd  19392  pmtrfb  19401  odmodnn0  19476  oddvdsnn0  19480  odnncl  19481  odmod  19482  oddvds  19483  odeq  19486  odmulgid  19490  odmulg  19492  odmulgeq  19493  odbezout  19494  odf1o1  19508  odf1o2  19509  odngen  19513  odcau  19540  pgpssslw  19550  fislw  19561  lsmless1x  19580  lsmless2x  19581  lsmsubm  19589  lsmmod  19611  lsmmod2  19612  efgsfo  19675  cntzcmn  19776  odadd1  19784  odadd2  19785  odadd  19786  lsmcomx  19792  prdscmnd  19797  gsumconst  19870  ring1eq0  20213  cntzsubrng  20482  cntzsubr  20521  isabvd  20727  rmodislmod  20842  lspss  20896  0lmhm  20953  reslmhm2  20966  pwssplit0  20971  pwssplit1  20972  lbspss  20995  lspfixed  21044  lsmcv  21057  lspsnat  21061  2idlcpblrng  21187  cnfldfunALT  21285  cnfldfunALTOLD  21298  xrsdsreclblem  21335  obselocv  21643  frlmsplit2  21688  frlmsslss2  21690  frlmup4  21716  lindff1  21735  lsslindf  21745  lsslinds  21746  islindf4  21753  issubassa  21782  aspss  21792  coe1subfv  22158  coe1tm  22165  mpomatmul  22339  mamutpos  22351  submaval  22474  mdetdiag  22492  mdetunilem1  22505  mdetunilem3  22507  mdetunilem9  22513  mdetmul  22516  maducoeval2  22533  madurid  22537  minmar1val  22541  cramer  22584  cpmatel2  22606  m2cpm  22634  decpmatmul  22665  pmatcollpw1lem2  22668  pmatcollpw1  22669  pmatcollpw2lem  22670  pm2mpcl  22690  mply1topmatcl  22698  mp2pm2mplem2  22700  mp2pm2mplem4  22702  pm2mpghmlem2  22705  pm2mpghmlem1  22706  cayhamlem2  22777  neiint  22997  topssnei  23017  cnrest2  23179  cnprest2  23183  cnt0  23239  cnt1  23243  cnhaus  23247  cncmp  23285  fiuncmp  23297  sscmp  23298  hauscmp  23300  cnconn  23315  unconn  23322  comppfsc  23425  kgen2ss  23448  ptpjopn  23505  ptrescn  23532  qtopss  23608  kqfvima  23623  r0cld  23631  cmphaushmeo  23693  fbssint  23731  fbasrn  23777  filuni  23778  ufilmax  23800  fin1aufil  23825  fmf  23838  fmss  23839  rnelfmlem  23845  rnelfm  23846  fmufil  23852  fmco  23854  flimss2  23865  flimss1  23866  flimrest  23876  cnpflf2  23893  cnpflf  23894  flfcnp  23897  lmflf  23898  supnfcls  23913  fclsss1  23915  fclsss2  23916  cnpfcfi  23933  subgntr  24000  opnsubg  24001  cldsubg  24004  ustuqtop1  24135  ucncn  24178  bldisj  24292  blgt0  24293  bl2in  24294  blss2ps  24297  blss2  24298  xbln0  24308  blssps  24318  blss  24319  lpbl  24397  blcld  24399  blcls  24400  stdbdmopn  24412  metcnp2  24436  txmetcnp  24441  blval2  24456  restmetu  24464  nmoix  24623  nmoi2  24624  nmoeq0  24630  nmotri  24633  metdsge  24744  metds0  24745  metdseq0  24749  icoopnst  24842  iccpnfhmeo  24849  xrhmeo  24850  nmhmcn  25026  cphsqrtcl2  25092  cphsqrtcl3  25093  fmcfil  25178  bcthlem5  25234  cmetcusp1  25259  cssbn  25281  pjth  25345  ovolunnul  25407  volun  25452  voliunlem2  25458  itg2const  25647  iblconst  25725  itgconst  25726  limcvallem  25778  dvcnp2  25827  dvcnp2OLD  25828  dvcn  25829  deg1mul3le  26028  deg1tmle  26029  idomrootle  26084  ig1pdvds  26091  coe11  26164  dgrmulc  26183  dvply1  26197  aaliou2  26254  efcvx  26365  tanord  26453  logdivlti  26535  logccv  26578  recxpcl  26590  cxplea  26611  cxple2a  26614  ang180  26730  isosctrlem2  26735  cxp2lim  26893  amgm  26907  muval1  27049  dvdssqf  27054  mumullem2  27096  bcmono  27194  lgsneg  27238  lgsmod  27240  lgsdirprm  27248  lgsdir  27249  lgsdi  27251  sltres  27580  nolt02olem  27612  nolt02o  27613  nogt01o  27614  nosupbnd1lem1  27626  nosupbnd1lem4  27629  nosupbnd1lem5  27630  nosupbnd1lem6  27631  noinfbnd1lem1  27641  noinfbnd1lem4  27644  noinfbnd1lem6  27646  noinfbnd2  27649  noetainflem3  27657  sltlpss  27825  cofsslt  27832  coinitsslt  27833  cofcutrtime  27841  addsass  27918  addsdi  28064  mulsass  28075  sltmul2  28080  norecdiv  28099  brbtwn2  28838  colinearalglem1  28839  colinearalg  28843  axcgrtr  28848  axcontlem2  28898  upgrewlkle2  29540  wlksoneq1eq2  29598  crctcshwlkn0lem5  29750  wspthsnwspthsnon  29852  lppthon  30086  upgriseupth  30142  4cyclusnfrgr  30227  numclwwlk1lem2foa  30289  numclwwlk5  30323  nvmul0or  30585  shless  31294  shlej1  31295  pjspansn  31512  kbmul  31890  homco2  31912  kbass2  32052  fnpreimac  32601  padct  32649  eliccelico  32706  elicoelioo  32707  iocinioc2  32708  difioo  32711  nexple  32775  swrdrn2  32882  swrdrn3  32883  xrge0npcan  32967  isarchi2  33145  archiabl  33158  pidlnz  33353  lindssn  33355  ssmxidl  33451  mdetlap1  33822  zarclsiin  33867  pstmfval  33892  fmcncfil  33927  zrhnm  33963  qqhnm  33986  volfiniune  34226  omsmeas  34320  eulerpartlemb  34365  probinc  34418  cndprob01  34432  signswmnd  34554  cvmsss2  35261  funsseq  35750  cgrtriv  35985  5segofs  35989  btwntriv2  35995  btwnxfr  36039  segcon2  36088  brsegle2  36092  seglelin  36099  outsideofeu  36114  weiunpo  36448  weiunfr  36450  weiunse  36451  lindsenlbs  37604  mblfinlem2  37647  blbnd  37776  rrndstprj2  37820  zerdivemp1x  37936  lsmsat  38996  lsatfixedN  38997  lssat  39004  lkrlsp  39090  lshpkrlem4  39101  cvrcon3b  39265  leat3  39283  atlen0  39298  atnle  39305  atlatmstc  39307  atlatle  39308  cvlcvr1  39327  cvlsupr2  39331  hlsupr2  39376  hlrelat2  39392  cvrexchlem  39408  cvratlem  39410  lnnat  39416  atexchcvrN  39429  1cvratlt  39463  1cvrjat  39464  3atlem3  39474  3atlem7  39478  llni2  39501  atcvrlln2  39508  llnexatN  39510  llncmp  39511  2llnmat  39513  2at0mat0  39514  2atnelpln  39533  llncvrlpln2  39546  2lplnmN  39548  2llnmj  39549  lplncmp  39551  lplnexatN  39552  2llnjaN  39555  lvoli3  39566  islvol2aN  39581  4atlem3a  39586  4atlem4a  39588  4atlem4b  39589  4atlem11  39598  4atlem12  39601  lplncvrlvol2  39604  lvolcmp  39606  2lplnmj  39611  islinei  39729  linepmap  39764  lneq2at  39767  2llnma3r  39777  elpaddn0  39789  elpaddatriN  39792  elpaddat  39793  paddcom  39802  paddss1  39806  paddss2  39807  paddasslem6  39814  paddasslem7  39815  paddasslem10  39818  paddasslem15  39823  pmodlem2  39836  pmodl42N  39840  pmapjoin  39841  atmod1i1m  39847  llnmod1i2  39849  llnexchb2lem  39857  polcon2bN  39909  pclfinclN  39939  poml4N  39942  poml6N  39944  osumcllem11N  39955  osumclN  39956  pmapojoinN  39957  pexmidlem2N  39960  pexmidlem3N  39961  pexmidlem4N  39962  pexmidlem6N  39964  pexmidlem7N  39965  pl42lem2N  39969  pl42lem3N  39970  pl42lem4N  39971  pl42N  39972  lhpexle3lem  40000  lhpmcvr3  40014  lhp2at0nle  40024  lhprelat3N  40029  lauteq  40084  lautco  40086  ltrncoidN  40117  ltrneq2  40137  ltrnnidn  40163  ltrnideq  40164  trlnle  40175  cdlemc  40186  cdlemd4  40190  cdlemd5  40191  cdlemd9  40195  cdlemd  40196  ltrneq3  40197  cdlemefrs29pre00  40384  cdlemefrs29cpre1  40387  cdlemefrs29clN  40388  cdlemefrs32fva  40389  cdlemefr29exN  40391  cdlemefr27cl  40392  cdlemefs27cl  40402  cdlemefs32sn1aw  40403  cdleme32fva  40426  cdleme32d  40433  cdleme32f  40435  cdleme32le  40436  cdleme40n  40457  cdleme41snaw  40465  cdleme17d3  40485  cdleme48fvg  40489  cdlemeg46fvcl  40495  cdlemeg46fgN  40523  cdleme48fgv  40527  ltrniotavalbN  40573  cdlemb3  40595  cdlemg15  40645  cdlemg17dN  40652  trlco  40716  cdlemg44b  40721  ltrncom  40727  trljco  40729  tendococl  40761  tendoplcl  40770  tendoplcom  40771  tendotr  40819  cdlemk36  40902  cdlemk35s-id  40927  cdlemk39s-id  40929  cdlemk19x  40932  cdlemk53b  40945  cdlemk55  40950  cdlemk35u  40953  cdlemk55u  40955  cdlemk39u  40957  cdlemk19u  40959  cdlemk56  40960  tendoex  40964  cdleml5N  40969  dihord2pre  41214  dihord6apre  41245  dihord5b  41248  dihord5apre  41251  dihord  41253  dihmeetlem1N  41279  dihmeetlem2N  41288  dihglbcpreN  41289  dihmeetbN  41292  dihmeetlem4preN  41295  dihmeetlem5  41297  dihmeetlem6  41298  dihmeetlem7N  41299  dihmeetlem10N  41305  dihmeetlem11N  41306  dihmeetlem12N  41307  dihmeetlem13N  41308  dihmeetlem15N  41310  dihmeetlem17N  41312  dihmeetlem18N  41313  dihmeetlem19N  41314  dihmeetALTN  41316  dih1dimatlem0  41317  dihlspsnssN  41321  dvh3dim2  41437  sticksstones1  42129  sticksstones2  42130  sticksstones12  42141  aks6d1c6isolem1  42157  dvdsexpnn  42316  resubcan2  42371  mzpsubst  42729  diophrw  42740  eldioph2lem1  42741  rencldnfi  42802  pellexlem2  42811  pellqrexplicit  42858  infmrgelbi  42859  rmxycomplete  42899  congadd  42948  acongeq  42965  jm2.19  42975  jm2.22  42977  jm2.20nn  42979  jm2.25lem1  42980  jm2.27  42990  jm3.1  43002  lmhmlnmsplit  43069  pwssplit4  43071  hbtlem2  43106  dgraa0p  43131  proot1hash  43177  iocunico  43193  cantnf2  43307  dflim5  43311  omcl2  43315  tfsconcatrn  43324  nadd2rabex  43368  relexpxpmin  43699  brtrclfv2  43709  ntrclsk3  44052  grur1cld  44214  ismnu  44243  suprnmpt  45161  wessf1ornlem  45172  choicefi  45187  supxrgere  45322  supxrgelem  45326  supxrge  45327  infleinflem2  45360  snunioo1  45503  iccintsng  45514  fmul01  45571  lptre2pt  45631  0ellimcdiv  45640  fnlimfvre  45665  limsupmnfuzlem  45717  climisp  45737  limsupgtlem  45768  ibliccsinexp  45942  iblioosinexp  45944  volioc  45963  iblspltprt  45964  stoweidlem20  46011  stoweidlem22  46013  stoweidlem34  46025  stoweidlem44  46035  stoweidlem60  46051  wallispilem3  46058  fourierdlem42  46140  fourierdlem51  46148  fourierdlem54  46151  fourierdlem87  46184  fourierdlem97  46194  ioorrnopnlem  46295  sge0seq  46437  hoicvr  46539  fsupdm  46833  finfdm  46837  3f1oss1  47066  funfocofob  47069  imasetpreimafvbijlemfv  47393  uhgrimisgrgric  47921  uhgrimgrlim  47976  fprmappr  48323  lincresunit3lem3  48453  lindssnlvec  48465  rrx2linesl  48722  line2  48731  itsclc0lem3  48737  itsclc0yqsollem1  48741  itscnhlc0xyqsol  48744  itschlc0xyqsol1  48745  itsclc0  48750  itscnhlinecirc02plem2  48762  itscnhlinecirc02plem3  48763  uptrlem1  49183  setc1onsubc  49571