Theorem simpl3 1200

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 483	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜒)
2	1	3ad2antl3 1194	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpl13  1257  simpl23  1260  simpl33  1263  simp1l3  1275  simp2l3  1281  simp3l3  1287  3anandirs  1480  2nreu  4379  predtrss  6280  frpomin  6298  f1prex  7235  fcofo  7239  soisores  7278  weniso  7305  knatar  7308  ofmpteq  7650  funelss  7996  frrlem10  8242  fprlem1  8247  smocdmdom  8305  nnmord  8565  nnmword  8566  naddasslem1  8627  naddasslem2  8628  difsnen  8994  mapunen  9081  ac6sfi  9191  fipreima  9265  wemaplem2  9459  wemapso2lem  9464  ttrclselem2  9645  en2eqpr  9927  indcardi  9961  acndom  9971  fodomfi2  9980  infmap2  10137  cflim2  10183  coftr  10193  infpssrlem4  10226  fin23lem11  10237  fincssdom  10243  isf32lem9  10281  fin1a2lem9  10328  gchpwdom  10591  gruima  10723  prpssnq  10911  distrlem4pr  10947  dedekind  11307  addcan  11328  addcan2  11329  divmulass  11830  supmul1  12123  uzsupss  12888  xaddass  13199  xleadd1a  13203  xlesubadd  13213  xmulasslem3  13236  xmulass  13237  xadddilem  13244  xadddi  13245  ixxun  13312  icoshftf1o  13425  snunioc  13431  difelfzle  13593  fzo1fzo0n0  13668  ssfzoulel  13713  modmuladd  13873  modifeq2int  13893  modaddmulmod  13898  modsubdir  13900  ltexp2a  14126  leexp2  14131  ltexp2r  14133  exple1  14137  expnlbnd2  14194  mulsubdivbinom2  14222  hashtpg  14445  ccatass  14549  ccatopth  14676  pfxccatin12lem2a  14687  pfxccat3  14694  cshinj  14771  2cshw  14773  s2f1o  14876  limsupgre  15441  addcn2  15554  mulcn2  15556  binomrisefac  16005  bpolydif  16018  dvdsmodexp  16227  modmulconst  16255  dvdsexp2im  16294  dvdsmod  16296  sadass  16438  gcdass  16514  rplpwr  16525  rpmulgcd2  16623  rpdvds  16627  rpexp  16690  prmdiveq  16754  hashgcdlem  16756  coprimeprodsq  16777  coprimeprodsq2  16778  pythagtriplem3  16787  pcdvdsb  16838  pcgcd1  16846  dvdsprmpweq  16853  pcbc  16869  0ram  16989  ramz2  16993  ramub1lem1  16995  mremre  17564  mrieqv2d  17603  lubun  18479  isnsgrp  18689  issubmnd  18727  frmdss2  18829  submefmnd  18861  sgrp2rid2ex  18896  mulgnn0p1  19059  mulgnnsubcl  19060  mulgneg  19066  mulgdirlem  19079  nmzsubg  19138  ghmmulg  19201  pmtrfv  19425  pmtrmvd  19429  pmtrfb  19438  odmodnn0  19513  oddvdsnn0  19517  odnncl  19518  odmod  19519  oddvds  19520  odeq  19523  odmulgid  19527  odmulg  19529  odmulgeq  19530  odbezout  19531  odf1o1  19545  odf1o2  19546  odngen  19550  odcau  19577  pgpssslw  19587  fislw  19598  lsmless1x  19617  lsmless2x  19618  lsmsubm  19626  lsmmod  19648  lsmmod2  19649  efgsfo  19712  cntzcmn  19813  odadd1  19821  odadd2  19822  odadd  19823  lsmcomx  19829  prdscmnd  19834  gsumconst  19907  ring1eq0  20277  cntzsubrng  20546  cntzsubr  20585  isabvd  20791  rmodislmod  20927  lspss  20981  0lmhm  21037  reslmhm2  21050  pwssplit0  21055  pwssplit1  21056  lbspss  21079  lspfixed  21128  lsmcv  21141  lspsnat  21145  2idlcpblrng  21271  cnfldfunALT  21369  xrsdsreclblem  21395  obselocv  21710  frlmsplit2  21755  frlmsslss2  21757  frlmup4  21783  lindff1  21802  lsslindf  21812  lsslinds  21813  islindf4  21820  issubassa  21849  aspss  21858  coe1subfv  22259  coe1tm  22266  mpomatmul  22436  mamutpos  22448  submaval  22571  mdetdiag  22589  mdetunilem1  22602  mdetunilem3  22604  mdetunilem9  22610  mdetmul  22613  maducoeval2  22630  madurid  22634  minmar1val  22638  cramer  22681  cpmatel2  22703  m2cpm  22731  decpmatmul  22762  pmatcollpw1lem2  22765  pmatcollpw1  22766  pmatcollpw2lem  22767  pm2mpcl  22787  mply1topmatcl  22795  mp2pm2mplem2  22797  mp2pm2mplem4  22799  pm2mpghmlem2  22802  pm2mpghmlem1  22803  cayhamlem2  22874  neiint  23094  topssnei  23114  cnrest2  23276  cnprest2  23280  cnt0  23336  cnt1  23340  cnhaus  23344  cncmp  23382  fiuncmp  23394  sscmp  23395  hauscmp  23397  cnconn  23412  unconn  23419  comppfsc  23522  kgen2ss  23545  ptpjopn  23602  ptrescn  23629  qtopss  23705  kqfvima  23720  r0cld  23728  cmphaushmeo  23790  fbssint  23828  fbasrn  23874  filuni  23875  ufilmax  23897  fin1aufil  23922  fmf  23935  fmss  23936  rnelfmlem  23942  rnelfm  23943  fmufil  23949  fmco  23951  flimss2  23962  flimss1  23963  flimrest  23973  cnpflf2  23990  cnpflf  23991  flfcnp  23994  lmflf  23995  supnfcls  24010  fclsss1  24012  fclsss2  24013  cnpfcfi  24030  subgntr  24097  opnsubg  24098  cldsubg  24101  ustuqtop1  24231  ucncn  24274  bldisj  24388  blgt0  24389  bl2in  24390  blss2ps  24393  blss2  24394  xbln0  24404  blssps  24414  blss  24415  lpbl  24493  blcld  24495  blcls  24496  stdbdmopn  24508  metcnp2  24532  txmetcnp  24537  blval2  24552  restmetu  24560  nmoix  24719  nmoi2  24720  nmoeq0  24726  nmotri  24729  metdsge  24840  metds0  24841  metdseq0  24845  icoopnst  24931  iccpnfhmeo  24937  xrhmeo  24938  nmhmcn  25112  cphsqrtcl2  25178  cphsqrtcl3  25179  fmcfil  25264  bcthlem5  25320  cmetcusp1  25345  cssbn  25367  pjth  25431  ovolunnul  25492  volun  25537  voliunlem2  25543  itg2const  25732  iblconst  25810  itgconst  25811  limcvallem  25863  dvcnp2  25912  dvcn  25913  deg1mul3le  26107  deg1tmle  26108  idomrootle  26163  ig1pdvds  26170  coe11  26243  dgrmulc  26261  dvply1  26275  aaliou2  26331  efcvx  26439  tanord  26527  logdivlti  26609  logccv  26652  recxpcl  26664  cxplea  26685  cxple2a  26688  ang180  26803  isosctrlem2  26808  cxp2lim  26965  amgm  26979  muval1  27121  dvdssqf  27126  mumullem2  27168  bcmono  27265  lgsneg  27309  lgsmod  27311  lgsdirprm  27319  lgsdir  27320  lgsdi  27322  ltsres  27651  nolt02olem  27683  nolt02o  27684  nogt01o  27685  nosupbnd1lem1  27697  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  noinfbnd1lem1  27712  noinfbnd1lem4  27715  noinfbnd1lem6  27717  noinfbnd2  27720  noetainflem3  27728  ltslpss  27925  cofslts  27935  coinitslts  27936  cofcutrtime  27944  addsass  28022  addsdi  28172  mulsass  28183  ltmuls2  28188  norecdiv  28207  z12bdaylem  28501  brbtwn2  28999  colinearalglem1  29000  colinearalg  29004  axcgrtr  29009  axcontlem2  29059  upgrewlkle2  29700  wlksoneq1eq2  29756  crctcshwlkn0lem5  29907  wspthsnwspthsnon  30009  lppthon  30246  upgriseupth  30302  4cyclusnfrgr  30387  numclwwlk1lem2foa  30449  numclwwlk5  30483  nvmul0or  30746  shless  31455  shlej1  31456  pjspansn  31673  kbmul  32051  homco2  32073  kbass2  32213  fnpreimac  32769  padct  32817  eliccelico  32876  elicoelioo  32877  iocinioc2  32878  difioo  32881  nexple  32943  swrdrn2  33040  swrdrn3  33041  xrge0npcan  33106  isarchi2  33273  archiabl  33286  pidlnz  33466  lindssn  33468  ssmxidl  33564  mdetlap1  34017  zarclsiin  34062  pstmfval  34087  fmcncfil  34122  zrhnm  34158  qqhnm  34181  volfiniune  34421  omsmeas  34514  eulerpartlemb  34559  probinc  34612  cndprob01  34626  signswmnd  34748  cvmsss2  35509  funsseq  36003  cgrtriv  36237  5segofs  36241  btwntriv2  36247  btwnxfr  36291  segcon2  36340  brsegle2  36344  seglelin  36351  outsideofeu  36366  weiunpo  36700  weiunfr  36702  weiunse  36703  lindsenlbs  37989  mblfinlem2  38032  blbnd  38161  rrndstprj2  38205  zerdivemp1x  38321  lsmsat  39507  lsatfixedN  39508  lssat  39515  lkrlsp  39601  lshpkrlem4  39612  cvrcon3b  39776  leat3  39794  atlen0  39809  atnle  39816  atlatmstc  39818  atlatle  39819  cvlcvr1  39838  cvlsupr2  39842  hlsupr2  39886  hlrelat2  39902  cvrexchlem  39918  cvratlem  39920  lnnat  39926  atexchcvrN  39939  1cvratlt  39973  1cvrjat  39974  3atlem3  39984  3atlem7  39988  llni2  40011  atcvrlln2  40018  llnexatN  40020  llncmp  40021  2llnmat  40023  2at0mat0  40024  2atnelpln  40043  llncvrlpln2  40056  2lplnmN  40058  2llnmj  40059  lplncmp  40061  lplnexatN  40062  2llnjaN  40065  lvoli3  40076  islvol2aN  40091  4atlem3a  40096  4atlem4a  40098  4atlem4b  40099  4atlem11  40108  4atlem12  40111  lplncvrlvol2  40114  lvolcmp  40116  2lplnmj  40121  islinei  40239  linepmap  40274  lneq2at  40277  2llnma3r  40287  elpaddn0  40299  elpaddatriN  40302  elpaddat  40303  paddcom  40312  paddss1  40316  paddss2  40317  paddasslem6  40324  paddasslem7  40325  paddasslem10  40328  paddasslem15  40333  pmodlem2  40346  pmodl42N  40350  pmapjoin  40351  atmod1i1m  40357  llnmod1i2  40359  llnexchb2lem  40367  polcon2bN  40419  pclfinclN  40449  poml4N  40452  poml6N  40454  osumcllem11N  40465  osumclN  40466  pmapojoinN  40467  pexmidlem2N  40470  pexmidlem3N  40471  pexmidlem4N  40472  pexmidlem6N  40474  pexmidlem7N  40475  pl42lem2N  40479  pl42lem3N  40480  pl42lem4N  40481  pl42N  40482  lhpexle3lem  40510  lhpmcvr3  40524  lhp2at0nle  40534  lhprelat3N  40539  lauteq  40594  lautco  40596  ltrncoidN  40627  ltrneq2  40647  ltrnnidn  40673  ltrnideq  40674  trlnle  40685  cdlemc  40696  cdlemd4  40700  cdlemd5  40701  cdlemd9  40705  cdlemd  40706  ltrneq3  40707  cdlemefrs29pre00  40894  cdlemefrs29cpre1  40897  cdlemefrs29clN  40898  cdlemefrs32fva  40899  cdlemefr29exN  40901  cdlemefr27cl  40902  cdlemefs27cl  40912  cdlemefs32sn1aw  40913  cdleme32fva  40936  cdleme32d  40943  cdleme32f  40945  cdleme32le  40946  cdleme40n  40967  cdleme41snaw  40975  cdleme17d3  40995  cdleme48fvg  40999  cdlemeg46fvcl  41005  cdlemeg46fgN  41033  cdleme48fgv  41037  ltrniotavalbN  41083  cdlemb3  41105  cdlemg15  41155  cdlemg17dN  41162  trlco  41226  cdlemg44b  41231  ltrncom  41237  trljco  41239  tendococl  41271  tendoplcl  41280  tendoplcom  41281  tendotr  41329  cdlemk36  41412  cdlemk35s-id  41437  cdlemk39s-id  41439  cdlemk19x  41442  cdlemk53b  41455  cdlemk55  41460  cdlemk35u  41463  cdlemk55u  41465  cdlemk39u  41467  cdlemk19u  41469  cdlemk56  41470  tendoex  41474  cdleml5N  41479  dihord2pre  41724  dihord6apre  41755  dihord5b  41758  dihord5apre  41761  dihord  41763  dihmeetlem1N  41789  dihmeetlem2N  41798  dihglbcpreN  41799  dihmeetbN  41802  dihmeetlem4preN  41805  dihmeetlem5  41807  dihmeetlem6  41808  dihmeetlem7N  41809  dihmeetlem10N  41815  dihmeetlem11N  41816  dihmeetlem12N  41817  dihmeetlem13N  41818  dihmeetlem15N  41820  dihmeetlem17N  41822  dihmeetlem18N  41823  dihmeetlem19N  41824  dihmeetALTN  41826  dih1dimatlem0  41827  dihlspsnssN  41831  dvh3dim2  41947  sticksstones1  42638  sticksstones2  42639  sticksstones12  42650  aks6d1c6isolem1  42666  dvdsexpnn  42817  resubcan2  42872  mzpsubst  43204  diophrw  43215  eldioph2lem1  43216  rencldnfi  43273  pellexlem2  43282  pellqrexplicit  43329  infmrgelbi  43330  rmxycomplete  43369  congadd  43418  acongeq  43435  jm2.19  43445  jm2.22  43447  jm2.20nn  43449  jm2.25lem1  43450  jm2.27  43460  jm3.1  43472  lmhmlnmsplit  43539  pwssplit4  43541  hbtlem2  43576  dgraa0p  43601  proot1hash  43647  iocunico  43663  cantnf2  43777  dflim5  43781  omcl2  43785  tfsconcatrn  43794  nadd2rabex  43838  relexpxpmin  44168  brtrclfv2  44178  ntrclsk3  44521  grur1cld  44683  ismnu  44712  suprnmpt  45628  wessf1ornlem  45639  choicefi  45653  supxrgere  45785  supxrgelem  45789  supxrge  45790  infleinflem2  45822  snunioo1  45964  iccintsng  45975  fmul01  46032  lptre2pt  46090  0ellimcdiv  46099  fnlimfvre  46124  limsupmnfuzlem  46176  climisp  46196  limsupgtlem  46227  ibliccsinexp  46401  iblioosinexp  46403  volioc  46422  iblspltprt  46423  stoweidlem20  46470  stoweidlem22  46472  stoweidlem34  46484  stoweidlem44  46494  stoweidlem60  46510  wallispilem3  46517  fourierdlem42  46599  fourierdlem51  46607  fourierdlem54  46610  fourierdlem87  46643  fourierdlem97  46653  ioorrnopnlem  46754  sge0seq  46896  hoicvr  46998  fsupdm  47292  finfdm  47296  3f1oss1  47545  funfocofob  47548  imasetpreimafvbijlemfv  47884  uhgrimisgrgric  48429  uhgrimgrlim  48485  fprmappr  48843  lincresunit3lem3  48972  lindssnlvec  48984  rrx2linesl  49241  line2  49250  itsclc0lem3  49256  itsclc0yqsollem1  49260  itscnhlc0xyqsol  49263  itschlc0xyqsol1  49264  itsclc0  49269  itscnhlinecirc02plem2  49281  itscnhlinecirc02plem3  49282  uptrlem1  49707  uptr2  49718  setc1onsubc  50099