Theorem simpl3 1192

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 1186	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  1249  simpl23  1252  simpl33  1255  simp1l3  1267  simp2l3  1273  simp3l3  1279  3anandirs  1471  2nreu  4449  predtrss  6344  frpomin  6362  f1prex  7303  fcofo  7307  soisores  7346  weniso  7373  knatar  7376  ofmpteq  7719  funelss  8070  frrlem10  8318  fprlem1  8323  smocdmdom  8406  nnmord  8668  nnmword  8669  naddasslem1  8730  naddasslem2  8731  difsnen  9091  mapunen  9184  ac6sfi  9317  fipreima  9395  wemaplem2  9584  wemapso2lem  9589  ttrclselem2  9763  en2eqpr  10044  indcardi  10078  acndom  10088  fodomfi2  10097  infmap2  10254  cflim2  10300  coftr  10310  infpssrlem4  10343  fin23lem11  10354  fincssdom  10360  isf32lem9  10398  fin1a2lem9  10445  gchpwdom  10707  gruima  10839  prpssnq  11027  distrlem4pr  11063  dedekind  11421  addcan  11442  addcan2  11443  divmulass  11942  supmul1  12234  uzsupss  12979  xaddass  13287  xleadd1a  13291  xlesubadd  13301  xmulasslem3  13324  xmulass  13325  xadddilem  13332  xadddi  13333  ixxun  13399  icoshftf1o  13510  snunioc  13516  difelfzle  13677  fzo1fzo0n0  13750  ssfzoulel  13795  modmuladd  13950  modifeq2int  13970  modaddmulmod  13975  modsubdir  13977  ltexp2a  14202  leexp2  14207  ltexp2r  14209  exple1  14212  expnlbnd2  14269  mulsubdivbinom2  14297  hashtpg  14520  ccatass  14622  ccatopth  14750  pfxccatin12lem2a  14761  pfxccat3  14768  cshinj  14845  2cshw  14847  s2f1o  14951  limsupgre  15513  addcn2  15626  mulcn2  15628  binomrisefac  16074  bpolydif  16087  dvdsmodexp  16294  modmulconst  16321  dvdsexp2im  16360  dvdsmod  16362  sadass  16504  gcdass  16580  rplpwr  16591  rpmulgcd2  16689  rpdvds  16693  rpexp  16755  prmdiveq  16819  hashgcdlem  16821  coprimeprodsq  16841  coprimeprodsq2  16842  pythagtriplem3  16851  pcdvdsb  16902  pcgcd1  16910  dvdsprmpweq  16917  pcbc  16933  0ram  17053  ramz2  17057  ramub1lem1  17059  mremre  17648  mrieqv2d  17683  lubun  18572  isnsgrp  18748  issubmnd  18786  frmdss2  18888  submefmnd  18920  sgrp2rid2ex  18952  mulgnn0p1  19115  mulgnnsubcl  19116  mulgneg  19122  mulgdirlem  19135  nmzsubg  19195  ghmmulg  19258  pmtrfv  19484  pmtrmvd  19488  pmtrfb  19497  odmodnn0  19572  oddvdsnn0  19576  odnncl  19577  odmod  19578  oddvds  19579  odeq  19582  odmulgid  19586  odmulg  19588  odmulgeq  19589  odbezout  19590  odf1o1  19604  odf1o2  19605  odngen  19609  odcau  19636  pgpssslw  19646  fislw  19657  lsmless1x  19676  lsmless2x  19677  lsmsubm  19685  lsmmod  19707  lsmmod2  19708  efgsfo  19771  cntzcmn  19872  odadd1  19880  odadd2  19881  odadd  19882  lsmcomx  19888  prdscmnd  19893  gsumconst  19966  ring1eq0  20311  cntzsubrng  20583  cntzsubr  20622  isabvd  20829  rmodislmod  20944  rmodislmodOLD  20945  lspss  20999  0lmhm  21056  reslmhm2  21069  pwssplit0  21074  pwssplit1  21075  lbspss  21098  lspfixed  21147  lsmcv  21160  lspsnat  21164  2idlcpblrng  21298  cnfldfunALT  21396  cnfldfunALTOLD  21409  xrsdsreclblem  21447  obselocv  21765  frlmsplit2  21810  frlmsslss2  21812  frlmup4  21838  lindff1  21857  lsslindf  21867  lsslinds  21868  islindf4  21875  issubassa  21904  aspss  21914  coe1subfv  22284  coe1tm  22291  mpomatmul  22467  mamutpos  22479  submaval  22602  mdetdiag  22620  mdetunilem1  22633  mdetunilem3  22635  mdetunilem9  22641  mdetmul  22644  maducoeval2  22661  madurid  22665  minmar1val  22669  cramer  22712  cpmatel2  22734  m2cpm  22762  decpmatmul  22793  pmatcollpw1lem2  22796  pmatcollpw1  22797  pmatcollpw2lem  22798  pm2mpcl  22818  mply1topmatcl  22826  mp2pm2mplem2  22828  mp2pm2mplem4  22830  pm2mpghmlem2  22833  pm2mpghmlem1  22834  cayhamlem2  22905  neiint  23127  topssnei  23147  cnrest2  23309  cnprest2  23313  cnt0  23369  cnt1  23373  cnhaus  23377  cncmp  23415  fiuncmp  23427  sscmp  23428  hauscmp  23430  cnconn  23445  unconn  23452  comppfsc  23555  kgen2ss  23578  ptpjopn  23635  ptrescn  23662  qtopss  23738  kqfvima  23753  r0cld  23761  cmphaushmeo  23823  fbssint  23861  fbasrn  23907  filuni  23908  ufilmax  23930  fin1aufil  23955  fmf  23968  fmss  23969  rnelfmlem  23975  rnelfm  23976  fmufil  23982  fmco  23984  flimss2  23995  flimss1  23996  flimrest  24006  cnpflf2  24023  cnpflf  24024  flfcnp  24027  lmflf  24028  supnfcls  24043  fclsss1  24045  fclsss2  24046  cnpfcfi  24063  subgntr  24130  opnsubg  24131  cldsubg  24134  ustuqtop1  24265  ucncn  24309  bldisj  24423  blgt0  24424  bl2in  24425  blss2ps  24428  blss2  24429  xbln0  24439  blssps  24449  blss  24450  lpbl  24531  blcld  24533  blcls  24534  stdbdmopn  24546  metcnp2  24570  txmetcnp  24575  blval2  24590  restmetu  24598  nmoix  24765  nmoi2  24766  nmoeq0  24772  nmotri  24775  metdsge  24884  metds0  24885  metdseq0  24889  icoopnst  24982  iccpnfhmeo  24989  xrhmeo  24990  nmhmcn  25166  cphsqrtcl2  25233  cphsqrtcl3  25234  fmcfil  25319  bcthlem5  25375  cmetcusp1  25400  cssbn  25422  pjth  25486  ovolunnul  25548  volun  25593  voliunlem2  25599  itg2const  25789  iblconst  25867  itgconst  25868  limcvallem  25920  dvcnp2  25969  dvcnp2OLD  25970  dvcn  25971  deg1mul3le  26170  deg1tmle  26171  idomrootle  26226  ig1pdvds  26233  coe11  26306  dgrmulc  26325  dvply1  26339  aaliou2  26396  efcvx  26507  tanord  26594  logdivlti  26676  logccv  26719  recxpcl  26731  cxplea  26752  cxple2a  26755  ang180  26871  isosctrlem2  26876  cxp2lim  27034  amgm  27048  muval1  27190  dvdssqf  27195  mumullem2  27237  bcmono  27335  lgsneg  27379  lgsmod  27381  lgsdirprm  27389  lgsdir  27390  lgsdi  27392  sltres  27721  nolt02olem  27753  nolt02o  27754  nogt01o  27755  nosupbnd1lem1  27767  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  noinfbnd1lem1  27782  noinfbnd1lem4  27785  noinfbnd1lem6  27787  noinfbnd2  27790  noetainflem3  27798  sltlpss  27959  cofsslt  27966  coinitsslt  27967  cofcutrtime  27975  addsass  28052  addsdi  28195  mulsass  28206  sltmul2  28211  norecdiv  28230  brbtwn2  28934  colinearalglem1  28935  colinearalg  28939  axcgrtr  28944  axcontlem2  28994  upgrewlkle2  29638  wlksoneq1eq2  29696  crctcshwlkn0lem5  29843  wspthsnwspthsnon  29945  lppthon  30179  upgriseupth  30235  4cyclusnfrgr  30320  numclwwlk1lem2foa  30382  numclwwlk5  30416  nvmul0or  30678  shless  31387  shlej1  31388  pjspansn  31605  kbmul  31983  homco2  32005  kbass2  32145  fnpreimac  32687  padct  32736  eliccelico  32785  elicoelioo  32786  iocinioc2  32787  difioo  32790  swrdrn2  32923  swrdrn3  32924  xrge0npcan  33007  isarchi2  33174  archiabl  33187  pidlnz  33383  lindssn  33385  ssmxidl  33481  mdetlap1  33786  zarclsiin  33831  pstmfval  33856  fmcncfil  33891  zrhnm  33929  qqhnm  33952  nexple  33989  volfiniune  34210  omsmeas  34304  eulerpartlemb  34349  probinc  34402  cndprob01  34416  signswmnd  34550  cvmsss2  35258  funsseq  35748  cgrtriv  35983  5segofs  35987  btwntriv2  35993  btwnxfr  36037  segcon2  36086  brsegle2  36090  seglelin  36097  outsideofeu  36112  weiunpo  36447  weiunfr  36449  weiunse  36450  lindsenlbs  37601  mblfinlem2  37644  blbnd  37773  rrndstprj2  37817  zerdivemp1x  37933  lsmsat  38989  lsatfixedN  38990  lssat  38997  lkrlsp  39083  lshpkrlem4  39094  cvrcon3b  39258  leat3  39276  atlen0  39291  atnle  39298  atlatmstc  39300  atlatle  39301  cvlcvr1  39320  cvlsupr2  39324  hlsupr2  39369  hlrelat2  39385  cvrexchlem  39401  cvratlem  39403  lnnat  39409  atexchcvrN  39422  1cvratlt  39456  1cvrjat  39457  3atlem3  39467  3atlem7  39471  llni2  39494  atcvrlln2  39501  llnexatN  39503  llncmp  39504  2llnmat  39506  2at0mat0  39507  2atnelpln  39526  llncvrlpln2  39539  2lplnmN  39541  2llnmj  39542  lplncmp  39544  lplnexatN  39545  2llnjaN  39548  lvoli3  39559  islvol2aN  39574  4atlem3a  39579  4atlem4a  39581  4atlem4b  39582  4atlem11  39591  4atlem12  39594  lplncvrlvol2  39597  lvolcmp  39599  2lplnmj  39604  islinei  39722  linepmap  39757  lneq2at  39760  2llnma3r  39770  elpaddn0  39782  elpaddatriN  39785  elpaddat  39786  paddcom  39795  paddss1  39799  paddss2  39800  paddasslem6  39807  paddasslem7  39808  paddasslem10  39811  paddasslem15  39816  pmodlem2  39829  pmodl42N  39833  pmapjoin  39834  atmod1i1m  39840  llnmod1i2  39842  llnexchb2lem  39850  polcon2bN  39902  pclfinclN  39932  poml4N  39935  poml6N  39937  osumcllem11N  39948  osumclN  39949  pmapojoinN  39950  pexmidlem2N  39953  pexmidlem3N  39954  pexmidlem4N  39955  pexmidlem6N  39957  pexmidlem7N  39958  pl42lem2N  39962  pl42lem3N  39963  pl42lem4N  39964  pl42N  39965  lhpexle3lem  39993  lhpmcvr3  40007  lhp2at0nle  40017  lhprelat3N  40022  lauteq  40077  lautco  40079  ltrncoidN  40110  ltrneq2  40130  ltrnnidn  40156  ltrnideq  40157  trlnle  40168  cdlemc  40179  cdlemd4  40183  cdlemd5  40184  cdlemd9  40188  cdlemd  40189  ltrneq3  40190  cdlemefrs29pre00  40377  cdlemefrs29cpre1  40380  cdlemefrs29clN  40381  cdlemefrs32fva  40382  cdlemefr29exN  40384  cdlemefr27cl  40385  cdlemefs27cl  40395  cdlemefs32sn1aw  40396  cdleme32fva  40419  cdleme32d  40426  cdleme32f  40428  cdleme32le  40429  cdleme40n  40450  cdleme41snaw  40458  cdleme17d3  40478  cdleme48fvg  40482  cdlemeg46fvcl  40488  cdlemeg46fgN  40516  cdleme48fgv  40520  ltrniotavalbN  40566  cdlemb3  40588  cdlemg15  40638  cdlemg17dN  40645  trlco  40709  cdlemg44b  40714  ltrncom  40720  trljco  40722  tendococl  40754  tendoplcl  40763  tendoplcom  40764  tendotr  40812  cdlemk36  40895  cdlemk35s-id  40920  cdlemk39s-id  40922  cdlemk19x  40925  cdlemk53b  40938  cdlemk55  40943  cdlemk35u  40946  cdlemk55u  40948  cdlemk39u  40950  cdlemk19u  40952  cdlemk56  40953  tendoex  40957  cdleml5N  40962  dihord2pre  41207  dihord6apre  41238  dihord5b  41241  dihord5apre  41244  dihord  41246  dihmeetlem1N  41272  dihmeetlem2N  41281  dihglbcpreN  41282  dihmeetbN  41285  dihmeetlem4preN  41288  dihmeetlem5  41290  dihmeetlem6  41291  dihmeetlem7N  41292  dihmeetlem10N  41298  dihmeetlem11N  41299  dihmeetlem12N  41300  dihmeetlem13N  41301  dihmeetlem15N  41303  dihmeetlem17N  41305  dihmeetlem18N  41306  dihmeetlem19N  41307  dihmeetALTN  41309  dih1dimatlem0  41310  dihlspsnssN  41314  dvh3dim2  41430  sticksstones1  42127  sticksstones2  42128  sticksstones12  42139  aks6d1c6isolem1  42155  dvdsexpnn  42346  resubcan2  42394  mzpsubst  42735  diophrw  42746  eldioph2lem1  42747  rencldnfi  42808  pellexlem2  42817  pellqrexplicit  42864  infmrgelbi  42865  rmxycomplete  42905  congadd  42954  acongeq  42971  jm2.19  42981  jm2.22  42983  jm2.20nn  42985  jm2.25lem1  42986  jm2.27  42996  jm3.1  43008  lmhmlnmsplit  43075  pwssplit4  43077  hbtlem2  43112  dgraa0p  43137  proot1hash  43183  iocunico  43199  cantnf2  43314  dflim5  43318  omcl2  43322  tfsconcatrn  43331  nadd2rabex  43375  relexpxpmin  43706  brtrclfv2  43716  ntrclsk3  44059  grur1cld  44227  ismnu  44256  suprnmpt  45116  wessf1ornlem  45127  choicefi  45142  supxrgere  45282  supxrgelem  45286  supxrge  45287  infleinflem2  45320  snunioo1  45464  iccintsng  45475  fmul01  45535  lptre2pt  45595  0ellimcdiv  45604  fnlimfvre  45629  limsupmnfuzlem  45681  climisp  45701  limsupgtlem  45732  ibliccsinexp  45906  iblioosinexp  45908  volioc  45927  iblspltprt  45928  stoweidlem20  45975  stoweidlem22  45977  stoweidlem34  45989  stoweidlem44  45999  stoweidlem60  46015  wallispilem3  46022  fourierdlem42  46104  fourierdlem51  46112  fourierdlem54  46115  fourierdlem87  46148  fourierdlem97  46158  ioorrnopnlem  46259  sge0seq  46401  hoicvr  46503  fsupdm  46797  finfdm  46801  3f1oss1  47024  funfocofob  47027  imasetpreimafvbijlemfv  47326  uhgrimisgrgric  47836  uhgrimgrlim  47889  fprmappr  48189  lincresunit3lem3  48319  lindssnlvec  48331  rrx2linesl  48592  line2  48601  itsclc0lem3  48607  itsclc0yqsollem1  48611  itscnhlc0xyqsol  48614  itschlc0xyqsol1  48615  itsclc0  48620  itscnhlinecirc02plem2  48632  itscnhlinecirc02plem3  48633