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  4410  predtrss  6298  frpomin  6316  f1prex  7262  fcofo  7266  soisores  7305  weniso  7332  knatar  7335  ofmpteq  7679  funelss  8029  frrlem10  8277  fprlem1  8282  smocdmdom  8340  nnmord  8599  nnmword  8600  naddasslem1  8661  naddasslem2  8662  difsnen  9027  mapunen  9116  ac6sfi  9238  fipreima  9316  wemaplem2  9507  wemapso2lem  9512  ttrclselem2  9686  en2eqpr  9967  indcardi  10001  acndom  10011  fodomfi2  10020  infmap2  10177  cflim2  10223  coftr  10233  infpssrlem4  10266  fin23lem11  10277  fincssdom  10283  isf32lem9  10321  fin1a2lem9  10368  gchpwdom  10630  gruima  10762  prpssnq  10950  distrlem4pr  10986  dedekind  11344  addcan  11365  addcan2  11366  divmulass  11867  supmul1  12159  uzsupss  12906  xaddass  13216  xleadd1a  13220  xlesubadd  13230  xmulasslem3  13253  xmulass  13254  xadddilem  13261  xadddi  13262  ixxun  13329  icoshftf1o  13442  snunioc  13448  difelfzle  13609  fzo1fzo0n0  13683  ssfzoulel  13728  modmuladd  13885  modifeq2int  13905  modaddmulmod  13910  modsubdir  13912  ltexp2a  14138  leexp2  14143  ltexp2r  14145  exple1  14149  expnlbnd2  14206  mulsubdivbinom2  14234  hashtpg  14457  ccatass  14560  ccatopth  14688  pfxccatin12lem2a  14699  pfxccat3  14706  cshinj  14783  2cshw  14785  s2f1o  14889  limsupgre  15454  addcn2  15567  mulcn2  15569  binomrisefac  16015  bpolydif  16028  dvdsmodexp  16237  modmulconst  16265  dvdsexp2im  16304  dvdsmod  16306  sadass  16448  gcdass  16524  rplpwr  16535  rpmulgcd2  16633  rpdvds  16637  rpexp  16699  prmdiveq  16763  hashgcdlem  16765  coprimeprodsq  16786  coprimeprodsq2  16787  pythagtriplem3  16796  pcdvdsb  16847  pcgcd1  16855  dvdsprmpweq  16862  pcbc  16878  0ram  16998  ramz2  17002  ramub1lem1  17004  mremre  17572  mrieqv2d  17607  lubun  18481  isnsgrp  18657  issubmnd  18695  frmdss2  18797  submefmnd  18829  sgrp2rid2ex  18861  mulgnn0p1  19024  mulgnnsubcl  19025  mulgneg  19031  mulgdirlem  19044  nmzsubg  19104  ghmmulg  19167  pmtrfv  19389  pmtrmvd  19393  pmtrfb  19402  odmodnn0  19477  oddvdsnn0  19481  odnncl  19482  odmod  19483  oddvds  19484  odeq  19487  odmulgid  19491  odmulg  19493  odmulgeq  19494  odbezout  19495  odf1o1  19509  odf1o2  19510  odngen  19514  odcau  19541  pgpssslw  19551  fislw  19562  lsmless1x  19581  lsmless2x  19582  lsmsubm  19590  lsmmod  19612  lsmmod2  19613  efgsfo  19676  cntzcmn  19777  odadd1  19785  odadd2  19786  odadd  19787  lsmcomx  19793  prdscmnd  19798  gsumconst  19871  ring1eq0  20214  cntzsubrng  20483  cntzsubr  20522  isabvd  20728  rmodislmod  20843  lspss  20897  0lmhm  20954  reslmhm2  20967  pwssplit0  20972  pwssplit1  20973  lbspss  20996  lspfixed  21045  lsmcv  21058  lspsnat  21062  2idlcpblrng  21188  cnfldfunALT  21286  cnfldfunALTOLD  21299  xrsdsreclblem  21336  obselocv  21644  frlmsplit2  21689  frlmsslss2  21691  frlmup4  21717  lindff1  21736  lsslindf  21746  lsslinds  21747  islindf4  21754  issubassa  21783  aspss  21793  coe1subfv  22159  coe1tm  22166  mpomatmul  22340  mamutpos  22352  submaval  22475  mdetdiag  22493  mdetunilem1  22506  mdetunilem3  22508  mdetunilem9  22514  mdetmul  22517  maducoeval2  22534  madurid  22538  minmar1val  22542  cramer  22585  cpmatel2  22607  m2cpm  22635  decpmatmul  22666  pmatcollpw1lem2  22669  pmatcollpw1  22670  pmatcollpw2lem  22671  pm2mpcl  22691  mply1topmatcl  22699  mp2pm2mplem2  22701  mp2pm2mplem4  22703  pm2mpghmlem2  22706  pm2mpghmlem1  22707  cayhamlem2  22778  neiint  22998  topssnei  23018  cnrest2  23180  cnprest2  23184  cnt0  23240  cnt1  23244  cnhaus  23248  cncmp  23286  fiuncmp  23298  sscmp  23299  hauscmp  23301  cnconn  23316  unconn  23323  comppfsc  23426  kgen2ss  23449  ptpjopn  23506  ptrescn  23533  qtopss  23609  kqfvima  23624  r0cld  23632  cmphaushmeo  23694  fbssint  23732  fbasrn  23778  filuni  23779  ufilmax  23801  fin1aufil  23826  fmf  23839  fmss  23840  rnelfmlem  23846  rnelfm  23847  fmufil  23853  fmco  23855  flimss2  23866  flimss1  23867  flimrest  23877  cnpflf2  23894  cnpflf  23895  flfcnp  23898  lmflf  23899  supnfcls  23914  fclsss1  23916  fclsss2  23917  cnpfcfi  23934  subgntr  24001  opnsubg  24002  cldsubg  24005  ustuqtop1  24136  ucncn  24179  bldisj  24293  blgt0  24294  bl2in  24295  blss2ps  24298  blss2  24299  xbln0  24309  blssps  24319  blss  24320  lpbl  24398  blcld  24400  blcls  24401  stdbdmopn  24413  metcnp2  24437  txmetcnp  24442  blval2  24457  restmetu  24465  nmoix  24624  nmoi2  24625  nmoeq0  24631  nmotri  24634  metdsge  24745  metds0  24746  metdseq0  24750  icoopnst  24843  iccpnfhmeo  24850  xrhmeo  24851  nmhmcn  25027  cphsqrtcl2  25093  cphsqrtcl3  25094  fmcfil  25179  bcthlem5  25235  cmetcusp1  25260  cssbn  25282  pjth  25346  ovolunnul  25408  volun  25453  voliunlem2  25459  itg2const  25648  iblconst  25726  itgconst  25727  limcvallem  25779  dvcnp2  25828  dvcnp2OLD  25829  dvcn  25830  deg1mul3le  26029  deg1tmle  26030  idomrootle  26085  ig1pdvds  26092  coe11  26165  dgrmulc  26184  dvply1  26198  aaliou2  26255  efcvx  26366  tanord  26454  logdivlti  26536  logccv  26579  recxpcl  26591  cxplea  26612  cxple2a  26615  ang180  26731  isosctrlem2  26736  cxp2lim  26894  amgm  26908  muval1  27050  dvdssqf  27055  mumullem2  27097  bcmono  27195  lgsneg  27239  lgsmod  27241  lgsdirprm  27249  lgsdir  27250  lgsdi  27252  sltres  27581  nolt02olem  27613  nolt02o  27614  nogt01o  27615  nosupbnd1lem1  27627  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  noinfbnd1lem1  27642  noinfbnd1lem4  27645  noinfbnd1lem6  27647  noinfbnd2  27650  noetainflem3  27658  sltlpss  27826  cofsslt  27833  coinitsslt  27834  cofcutrtime  27842  addsass  27919  addsdi  28065  mulsass  28076  sltmul2  28081  norecdiv  28100  brbtwn2  28839  colinearalglem1  28840  colinearalg  28844  axcgrtr  28849  axcontlem2  28899  upgrewlkle2  29541  wlksoneq1eq2  29599  crctcshwlkn0lem5  29751  wspthsnwspthsnon  29853  lppthon  30087  upgriseupth  30143  4cyclusnfrgr  30228  numclwwlk1lem2foa  30290  numclwwlk5  30324  nvmul0or  30586  shless  31295  shlej1  31296  pjspansn  31513  kbmul  31891  homco2  31913  kbass2  32053  fnpreimac  32602  padct  32650  eliccelico  32707  elicoelioo  32708  iocinioc2  32709  difioo  32712  nexple  32776  swrdrn2  32883  swrdrn3  32884  xrge0npcan  32968  isarchi2  33146  archiabl  33159  pidlnz  33354  lindssn  33356  ssmxidl  33452  mdetlap1  33823  zarclsiin  33868  pstmfval  33893  fmcncfil  33928  zrhnm  33964  qqhnm  33987  volfiniune  34227  omsmeas  34321  eulerpartlemb  34366  probinc  34419  cndprob01  34433  signswmnd  34555  cvmsss2  35268  funsseq  35762  cgrtriv  35997  5segofs  36001  btwntriv2  36007  btwnxfr  36051  segcon2  36100  brsegle2  36104  seglelin  36111  outsideofeu  36126  weiunpo  36460  weiunfr  36462  weiunse  36463  lindsenlbs  37616  mblfinlem2  37659  blbnd  37788  rrndstprj2  37832  zerdivemp1x  37948  lsmsat  39008  lsatfixedN  39009  lssat  39016  lkrlsp  39102  lshpkrlem4  39113  cvrcon3b  39277  leat3  39295  atlen0  39310  atnle  39317  atlatmstc  39319  atlatle  39320  cvlcvr1  39339  cvlsupr2  39343  hlsupr2  39388  hlrelat2  39404  cvrexchlem  39420  cvratlem  39422  lnnat  39428  atexchcvrN  39441  1cvratlt  39475  1cvrjat  39476  3atlem3  39486  3atlem7  39490  llni2  39513  atcvrlln2  39520  llnexatN  39522  llncmp  39523  2llnmat  39525  2at0mat0  39526  2atnelpln  39545  llncvrlpln2  39558  2lplnmN  39560  2llnmj  39561  lplncmp  39563  lplnexatN  39564  2llnjaN  39567  lvoli3  39578  islvol2aN  39593  4atlem3a  39598  4atlem4a  39600  4atlem4b  39601  4atlem11  39610  4atlem12  39613  lplncvrlvol2  39616  lvolcmp  39618  2lplnmj  39623  islinei  39741  linepmap  39776  lneq2at  39779  2llnma3r  39789  elpaddn0  39801  elpaddatriN  39804  elpaddat  39805  paddcom  39814  paddss1  39818  paddss2  39819  paddasslem6  39826  paddasslem7  39827  paddasslem10  39830  paddasslem15  39835  pmodlem2  39848  pmodl42N  39852  pmapjoin  39853  atmod1i1m  39859  llnmod1i2  39861  llnexchb2lem  39869  polcon2bN  39921  pclfinclN  39951  poml4N  39954  poml6N  39956  osumcllem11N  39967  osumclN  39968  pmapojoinN  39969  pexmidlem2N  39972  pexmidlem3N  39973  pexmidlem4N  39974  pexmidlem6N  39976  pexmidlem7N  39977  pl42lem2N  39981  pl42lem3N  39982  pl42lem4N  39983  pl42N  39984  lhpexle3lem  40012  lhpmcvr3  40026  lhp2at0nle  40036  lhprelat3N  40041  lauteq  40096  lautco  40098  ltrncoidN  40129  ltrneq2  40149  ltrnnidn  40175  ltrnideq  40176  trlnle  40187  cdlemc  40198  cdlemd4  40202  cdlemd5  40203  cdlemd9  40207  cdlemd  40208  ltrneq3  40209  cdlemefrs29pre00  40396  cdlemefrs29cpre1  40399  cdlemefrs29clN  40400  cdlemefrs32fva  40401  cdlemefr29exN  40403  cdlemefr27cl  40404  cdlemefs27cl  40414  cdlemefs32sn1aw  40415  cdleme32fva  40438  cdleme32d  40445  cdleme32f  40447  cdleme32le  40448  cdleme40n  40469  cdleme41snaw  40477  cdleme17d3  40497  cdleme48fvg  40501  cdlemeg46fvcl  40507  cdlemeg46fgN  40535  cdleme48fgv  40539  ltrniotavalbN  40585  cdlemb3  40607  cdlemg15  40657  cdlemg17dN  40664  trlco  40728  cdlemg44b  40733  ltrncom  40739  trljco  40741  tendococl  40773  tendoplcl  40782  tendoplcom  40783  tendotr  40831  cdlemk36  40914  cdlemk35s-id  40939  cdlemk39s-id  40941  cdlemk19x  40944  cdlemk53b  40957  cdlemk55  40962  cdlemk35u  40965  cdlemk55u  40967  cdlemk39u  40969  cdlemk19u  40971  cdlemk56  40972  tendoex  40976  cdleml5N  40981  dihord2pre  41226  dihord6apre  41257  dihord5b  41260  dihord5apre  41263  dihord  41265  dihmeetlem1N  41291  dihmeetlem2N  41300  dihglbcpreN  41301  dihmeetbN  41304  dihmeetlem4preN  41307  dihmeetlem5  41309  dihmeetlem6  41310  dihmeetlem7N  41311  dihmeetlem10N  41317  dihmeetlem11N  41318  dihmeetlem12N  41319  dihmeetlem13N  41320  dihmeetlem15N  41322  dihmeetlem17N  41324  dihmeetlem18N  41325  dihmeetlem19N  41326  dihmeetALTN  41328  dih1dimatlem0  41329  dihlspsnssN  41333  dvh3dim2  41449  sticksstones1  42141  sticksstones2  42142  sticksstones12  42153  aks6d1c6isolem1  42169  dvdsexpnn  42328  resubcan2  42383  mzpsubst  42743  diophrw  42754  eldioph2lem1  42755  rencldnfi  42816  pellexlem2  42825  pellqrexplicit  42872  infmrgelbi  42873  rmxycomplete  42913  congadd  42962  acongeq  42979  jm2.19  42989  jm2.22  42991  jm2.20nn  42993  jm2.25lem1  42994  jm2.27  43004  jm3.1  43016  lmhmlnmsplit  43083  pwssplit4  43085  hbtlem2  43120  dgraa0p  43145  proot1hash  43191  iocunico  43207  cantnf2  43321  dflim5  43325  omcl2  43329  tfsconcatrn  43338  nadd2rabex  43382  relexpxpmin  43713  brtrclfv2  43723  ntrclsk3  44066  grur1cld  44228  ismnu  44257  suprnmpt  45175  wessf1ornlem  45186  choicefi  45201  supxrgere  45336  supxrgelem  45340  supxrge  45341  infleinflem2  45374  snunioo1  45517  iccintsng  45528  fmul01  45585  lptre2pt  45645  0ellimcdiv  45654  fnlimfvre  45679  limsupmnfuzlem  45731  climisp  45751  limsupgtlem  45782  ibliccsinexp  45956  iblioosinexp  45958  volioc  45977  iblspltprt  45978  stoweidlem20  46025  stoweidlem22  46027  stoweidlem34  46039  stoweidlem44  46049  stoweidlem60  46065  wallispilem3  46072  fourierdlem42  46154  fourierdlem51  46162  fourierdlem54  46165  fourierdlem87  46198  fourierdlem97  46208  ioorrnopnlem  46309  sge0seq  46451  hoicvr  46553  fsupdm  46847  finfdm  46851  3f1oss1  47080  funfocofob  47083  imasetpreimafvbijlemfv  47407  uhgrimisgrgric  47935  uhgrimgrlim  47990  fprmappr  48337  lincresunit3lem3  48467  lindssnlvec  48479  rrx2linesl  48736  line2  48745  itsclc0lem3  48751  itsclc0yqsollem1  48755  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclc0  48764  itscnhlinecirc02plem2  48776  itscnhlinecirc02plem3  48777  uptrlem1  49203  uptr2  49214  setc1onsubc  49595