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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl13  1250  simpl23  1253  simpl33  1256  simp1l3  1268  simp2l3  1274  simp3l3  1280  3anandirs  1472  2nreu  4441  predtrss  6323  frpomin  6341  f1prex  7284  fcofo  7288  soisores  7326  weniso  7353  knatar  7356  ofmpteq  7694  funelss  8035  frrlem10  8282  fprlem1  8287  smocdmdom  8370  nnmord  8634  nnmword  8635  naddasslem1  8695  naddasslem2  8696  difsnen  9055  mapunen  9148  ac6sfi  9289  fipreima  9360  wemaplem2  9544  wemapso2lem  9549  ttrclselem2  9723  en2eqpr  10004  indcardi  10038  acndom  10048  fodomfi2  10057  infmap2  10215  cflim2  10260  coftr  10270  infpssrlem4  10303  fin23lem11  10314  fincssdom  10320  isf32lem9  10358  fin1a2lem9  10405  gchpwdom  10667  gruima  10799  prpssnq  10987  distrlem4pr  11023  dedekind  11381  addcan  11402  addcan2  11403  divmulass  11899  supmul1  12187  uzsupss  12928  xaddass  13232  xleadd1a  13236  xlesubadd  13246  xmulasslem3  13269  xmulass  13270  xadddilem  13277  xadddi  13278  ixxun  13344  icoshftf1o  13455  snunioc  13461  difelfzle  13618  fzo1fzo0n0  13687  ssfzoulel  13730  modmuladd  13882  modifeq2int  13902  modaddmulmod  13907  modsubdir  13909  ltexp2a  14135  leexp2  14140  ltexp2r  14142  exple1  14145  expnlbnd2  14201  mulsubdivbinom2  14226  hashtpg  14450  ccatass  14542  ccatopth  14670  pfxccatin12lem2a  14681  pfxccat3  14688  cshinj  14765  2cshw  14767  s2f1o  14871  limsupgre  15429  addcn2  15542  mulcn2  15544  binomrisefac  15990  bpolydif  16003  dvdsmodexp  16209  modmulconst  16235  dvdsexp2im  16274  dvdsmod  16276  sadass  16416  gcdass  16493  rplpwr  16503  rpmulgcd2  16597  rpdvds  16601  rpexp  16663  prmdiveq  16723  hashgcdlem  16725  coprimeprodsq  16745  coprimeprodsq2  16746  pythagtriplem3  16755  pcdvdsb  16806  pcgcd1  16814  dvdsprmpweq  16821  pcbc  16837  0ram  16957  ramz2  16961  ramub1lem1  16963  mremre  17552  mrieqv2d  17587  lubun  18472  isnsgrp  18648  issubmnd  18686  frmdss2  18780  submefmnd  18812  sgrp2rid2ex  18844  mulgnn0p1  19001  mulgnnsubcl  19002  mulgneg  19008  mulgdirlem  19021  nmzsubg  19081  ghmmulg  19142  pmtrfv  19361  pmtrmvd  19365  pmtrfb  19374  odmodnn0  19449  oddvdsnn0  19453  odnncl  19454  odmod  19455  oddvds  19456  odeq  19459  odmulgid  19463  odmulg  19465  odmulgeq  19466  odbezout  19467  odf1o1  19481  odf1o2  19482  odngen  19486  odcau  19513  pgpssslw  19523  fislw  19534  lsmless1x  19553  lsmless2x  19554  lsmsubm  19562  lsmmod  19584  lsmmod2  19585  efgsfo  19648  cntzcmn  19749  odadd1  19757  odadd2  19758  odadd  19759  lsmcomx  19765  prdscmnd  19770  gsumconst  19843  ring1eq0  20186  cntzsubrng  20455  cntzsubr  20496  isabvd  20571  rmodislmod  20684  rmodislmodOLD  20685  lspss  20739  0lmhm  20795  reslmhm2  20808  pwssplit0  20813  pwssplit1  20814  lbspss  20837  lspfixed  20886  lsmcv  20899  lspsnat  20903  2idlcpblrng  21020  cnfldfunALT  21157  xrsdsreclblem  21191  obselocv  21502  frlmsplit2  21547  frlmsslss2  21549  frlmup4  21575  lindff1  21594  lsslindf  21604  lsslinds  21605  islindf4  21612  issubassa  21640  aspss  21650  coe1subfv  22008  coe1tm  22015  mpomatmul  22168  mamutpos  22180  submaval  22303  mdetdiag  22321  mdetunilem1  22334  mdetunilem3  22336  mdetunilem9  22342  mdetmul  22345  maducoeval2  22362  madurid  22366  minmar1val  22370  cramer  22413  cpmatel2  22435  m2cpm  22463  decpmatmul  22494  pmatcollpw1lem2  22497  pmatcollpw1  22498  pmatcollpw2lem  22499  pm2mpcl  22519  mply1topmatcl  22527  mp2pm2mplem2  22529  mp2pm2mplem4  22531  pm2mpghmlem2  22534  pm2mpghmlem1  22535  cayhamlem2  22606  neiint  22828  topssnei  22848  cnrest2  23010  cnprest2  23014  cnt0  23070  cnt1  23074  cnhaus  23078  cncmp  23116  fiuncmp  23128  sscmp  23129  hauscmp  23131  cnconn  23146  unconn  23153  comppfsc  23256  kgen2ss  23279  ptpjopn  23336  ptrescn  23363  qtopss  23439  kqfvima  23454  r0cld  23462  cmphaushmeo  23524  fbssint  23562  fbasrn  23608  filuni  23609  ufilmax  23631  fin1aufil  23656  fmf  23669  fmss  23670  rnelfmlem  23676  rnelfm  23677  fmufil  23683  fmco  23685  flimss2  23696  flimss1  23697  flimrest  23707  cnpflf2  23724  cnpflf  23725  flfcnp  23728  lmflf  23729  supnfcls  23744  fclsss1  23746  fclsss2  23747  cnpfcfi  23764  subgntr  23831  opnsubg  23832  cldsubg  23835  ustuqtop1  23966  ucncn  24010  bldisj  24124  blgt0  24125  bl2in  24126  blss2ps  24129  blss2  24130  xbln0  24140  blssps  24150  blss  24151  lpbl  24232  blcld  24234  blcls  24235  stdbdmopn  24247  metcnp2  24271  txmetcnp  24276  blval2  24291  restmetu  24299  nmoix  24466  nmoi2  24467  nmoeq0  24473  nmotri  24476  metdsge  24585  metds0  24586  metdseq0  24590  icoopnst  24679  iccpnfhmeo  24685  xrhmeo  24686  nmhmcn  24860  cphsqrtcl2  24927  cphsqrtcl3  24928  fmcfil  25013  bcthlem5  25069  cmetcusp1  25094  cssbn  25116  pjth  25180  ovolunnul  25241  volun  25286  voliunlem2  25292  itg2const  25482  iblconst  25559  itgconst  25560  limcvallem  25612  dvcnp2  25661  dvcn  25662  deg1mul3le  25858  deg1tmle  25859  ig1pdvds  25918  coe11  25991  dgrmulc  26009  dvply1  26021  aaliou2  26077  efcvx  26185  tanord  26271  logdivlti  26352  logccv  26395  recxpcl  26407  cxplea  26428  cxple2a  26431  ang180  26543  isosctrlem2  26548  cxp2lim  26705  amgm  26719  muval1  26861  dvdssqf  26866  mumullem2  26908  bcmono  27004  lgsneg  27048  lgsmod  27050  lgsdirprm  27058  lgsdir  27059  lgsdi  27061  sltres  27389  nolt02olem  27421  nolt02o  27422  nogt01o  27423  nosupbnd1lem1  27435  nosupbnd1lem4  27438  nosupbnd1lem5  27439  nosupbnd1lem6  27440  noinfbnd1lem1  27450  noinfbnd1lem4  27453  noinfbnd1lem6  27455  noinfbnd2  27458  noetainflem3  27466  sltlpss  27626  cofsslt  27631  coinitsslt  27632  cofcutrtime  27640  addsass  27715  addsdi  27837  mulsass  27848  sltmul2  27850  norecdiv  27865  brbtwn2  28418  colinearalglem1  28419  colinearalg  28423  axcgrtr  28428  axcontlem2  28478  upgrewlkle2  29118  wlksoneq1eq2  29176  crctcshwlkn0lem5  29323  wspthsnwspthsnon  29425  lppthon  29659  upgriseupth  29715  4cyclusnfrgr  29800  numclwwlk1lem2foa  29862  numclwwlk5  29896  nvmul0or  30158  shless  30867  shlej1  30868  pjspansn  31085  kbmul  31463  homco2  31485  kbass2  31625  fnpreimac  32151  padct  32199  eliccelico  32243  elicoelioo  32244  iocinioc2  32245  difioo  32248  swrdrn2  32373  swrdrn3  32374  xrge0npcan  32450  isarchi2  32589  archiabl  32602  pidlnz  32750  lindssn  32756  ssmxidl  32852  mdetlap1  33092  zarclsiin  33137  pstmfval  33162  fmcncfil  33197  zrhnm  33235  qqhnm  33256  nexple  33293  volfiniune  33514  omsmeas  33608  eulerpartlemb  33653  probinc  33706  cndprob01  33720  signswmnd  33854  cvmsss2  34551  funsseq  35031  cgrtriv  35266  5segofs  35270  btwntriv2  35276  btwnxfr  35320  segcon2  35369  brsegle2  35373  seglelin  35380  outsideofeu  35395  gg-dvcnp2  35460  gg-cnfldfunALT  35484  lindsenlbs  36786  mblfinlem2  36829  blbnd  36958  rrndstprj2  37002  zerdivemp1x  37118  lsmsat  38181  lsatfixedN  38182  lssat  38189  lkrlsp  38275  lshpkrlem4  38286  cvrcon3b  38450  leat3  38468  atlen0  38483  atnle  38490  atlatmstc  38492  atlatle  38493  cvlcvr1  38512  cvlsupr2  38516  hlsupr2  38561  hlrelat2  38577  cvrexchlem  38593  cvratlem  38595  lnnat  38601  atexchcvrN  38614  1cvratlt  38648  1cvrjat  38649  3atlem3  38659  3atlem7  38663  llni2  38686  atcvrlln2  38693  llnexatN  38695  llncmp  38696  2llnmat  38698  2at0mat0  38699  2atnelpln  38718  llncvrlpln2  38731  2lplnmN  38733  2llnmj  38734  lplncmp  38736  lplnexatN  38737  2llnjaN  38740  lvoli3  38751  islvol2aN  38766  4atlem3a  38771  4atlem4a  38773  4atlem4b  38774  4atlem11  38783  4atlem12  38786  lplncvrlvol2  38789  lvolcmp  38791  2lplnmj  38796  islinei  38914  linepmap  38949  lneq2at  38952  2llnma3r  38962  elpaddn0  38974  elpaddatriN  38977  elpaddat  38978  paddcom  38987  paddss1  38991  paddss2  38992  paddasslem6  38999  paddasslem7  39000  paddasslem10  39003  paddasslem15  39008  pmodlem2  39021  pmodl42N  39025  pmapjoin  39026  atmod1i1m  39032  llnmod1i2  39034  llnexchb2lem  39042  polcon2bN  39094  pclfinclN  39124  poml4N  39127  poml6N  39129  osumcllem11N  39140  osumclN  39141  pmapojoinN  39142  pexmidlem2N  39145  pexmidlem3N  39146  pexmidlem4N  39147  pexmidlem6N  39149  pexmidlem7N  39150  pl42lem2N  39154  pl42lem3N  39155  pl42lem4N  39156  pl42N  39157  lhpexle3lem  39185  lhpmcvr3  39199  lhp2at0nle  39209  lhprelat3N  39214  lauteq  39269  lautco  39271  ltrncoidN  39302  ltrneq2  39322  ltrnnidn  39348  ltrnideq  39349  trlnle  39360  cdlemc  39371  cdlemd4  39375  cdlemd5  39376  cdlemd9  39380  cdlemd  39381  ltrneq3  39382  cdlemefrs29pre00  39569  cdlemefrs29cpre1  39572  cdlemefrs29clN  39573  cdlemefrs32fva  39574  cdlemefr29exN  39576  cdlemefr27cl  39577  cdlemefs27cl  39587  cdlemefs32sn1aw  39588  cdleme32fva  39611  cdleme32d  39618  cdleme32f  39620  cdleme32le  39621  cdleme40n  39642  cdleme41snaw  39650  cdleme17d3  39670  cdleme48fvg  39674  cdlemeg46fvcl  39680  cdlemeg46fgN  39708  cdleme48fgv  39712  ltrniotavalbN  39758  cdlemb3  39780  cdlemg15  39830  cdlemg17dN  39837  trlco  39901  cdlemg44b  39906  ltrncom  39912  trljco  39914  tendococl  39946  tendoplcl  39955  tendoplcom  39956  tendotr  40004  cdlemk36  40087  cdlemk35s-id  40112  cdlemk39s-id  40114  cdlemk19x  40117  cdlemk53b  40130  cdlemk55  40135  cdlemk35u  40138  cdlemk55u  40140  cdlemk39u  40142  cdlemk19u  40144  cdlemk56  40145  tendoex  40149  cdleml5N  40154  dihord2pre  40399  dihord6apre  40430  dihord5b  40433  dihord5apre  40436  dihord  40438  dihmeetlem1N  40464  dihmeetlem2N  40473  dihglbcpreN  40474  dihmeetbN  40477  dihmeetlem4preN  40480  dihmeetlem5  40482  dihmeetlem6  40483  dihmeetlem7N  40484  dihmeetlem10N  40490  dihmeetlem11N  40491  dihmeetlem12N  40492  dihmeetlem13N  40493  dihmeetlem15N  40495  dihmeetlem17N  40497  dihmeetlem18N  40498  dihmeetlem19N  40499  dihmeetALTN  40501  dih1dimatlem0  40502  dihlspsnssN  40506  dvh3dim2  40622  sticksstones1  41268  sticksstones2  41269  sticksstones12  41280  dvdsexpnn  41533  resubcan2  41563  mzpsubst  41788  diophrw  41799  eldioph2lem1  41800  rencldnfi  41861  pellexlem2  41870  pellqrexplicit  41917  infmrgelbi  41918  rmxycomplete  41958  congadd  42007  acongeq  42024  jm2.19  42034  jm2.22  42036  jm2.20nn  42038  jm2.25lem1  42039  jm2.27  42049  jm3.1  42061  lmhmlnmsplit  42131  pwssplit4  42133  hbtlem2  42168  dgraa0p  42193  idomrootle  42239  proot1hash  42244  iocunico  42262  cantnf2  42377  dflim5  42381  omcl2  42385  tfsconcatrn  42394  nadd2rabex  42438  relexpxpmin  42770  brtrclfv2  42780  ntrclsk3  43123  grur1cld  43293  ismnu  43322  suprnmpt  44172  wessf1ornlem  44183  choicefi  44198  supxrgere  44342  supxrgelem  44346  supxrge  44347  infleinflem2  44380  snunioo1  44524  iccintsng  44535  fmul01  44595  lptre2pt  44655  0ellimcdiv  44664  fnlimfvre  44689  limsupmnfuzlem  44741  climisp  44761  limsupgtlem  44792  ibliccsinexp  44966  iblioosinexp  44968  volioc  44987  iblspltprt  44988  stoweidlem20  45035  stoweidlem22  45037  stoweidlem34  45049  stoweidlem44  45059  stoweidlem60  45075  wallispilem3  45082  fourierdlem42  45164  fourierdlem51  45172  fourierdlem54  45175  fourierdlem87  45208  fourierdlem97  45218  ioorrnopnlem  45319  sge0seq  45461  hoicvr  45563  fsupdm  45857  finfdm  45861  funfocofob  46085  imasetpreimafvbijlemfv  46369  fprmappr  47110  lincresunit3lem3  47243  lindssnlvec  47255  rrx2linesl  47517  line2  47526  itsclc0lem3  47532  itsclc0yqsollem1  47536  itscnhlc0xyqsol  47539  itschlc0xyqsol1  47540  itsclc0  47545  itscnhlinecirc02plem2  47557  itscnhlinecirc02plem3  47558