Theorem simpl3 1189

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  simpl13  1246  simpl23  1249  simpl33  1252  simp1l3  1264  simp2l3  1270  simp3l3  1276  3anandirs  1468  2nreu  4395  f1prex  7042  fcofo  7046  soisores  7082  weniso  7109  knatar  7112  ofmpteq  7430  funelss  7748  smorndom  8007  nnmord  8260  nnmword  8261  difsnen  8601  mapunen  8688  ac6sfi  8764  fipreima  8832  wemaplem2  9013  wemapso2lem  9018  en2eqpr  9435  indcardi  9469  acndom  9479  fodomfi2  9488  infmap2  9642  cflim2  9687  coftr  9697  infpssrlem4  9730  fin23lem11  9741  fincssdom  9747  isf32lem9  9785  fin1a2lem9  9832  gchpwdom  10094  gruima  10226  prpssnq  10414  distrlem4pr  10450  dedekind  10805  addcan  10826  addcan2  10827  divmulass  11323  supmul1  11612  uzsupss  12343  xaddass  12645  xleadd1a  12649  xlesubadd  12659  xmulasslem3  12682  xmulass  12683  xadddilem  12690  xadddi  12691  ixxun  12757  icoshftf1o  12863  snunioc  12869  difelfzle  13023  fzo1fzo0n0  13091  ssfzoulel  13134  modmuladd  13284  modifeq2int  13304  modaddmulmod  13309  modsubdir  13311  ltexp2a  13533  leexp2  13538  ltexp2r  13540  exple1  13543  expnlbnd2  13598  mulsubdivbinom2  13625  hashtpg  13846  ccatass  13944  ccatopth  14080  pfxccatin12lem2a  14091  pfxccat3  14098  cshinj  14175  2cshw  14177  s2f1o  14280  limsupgre  14840  addcn2  14952  mulcn2  14954  binomrisefac  15398  bpolydif  15411  dvdsmodexp  15617  modmulconst  15643  dvdsmod  15680  sadass  15822  gcdass  15897  rplpwr  15909  rppwr  15910  rpmulgcd2  16002  rpdvds  16006  rpexp  16066  prmdiveq  16125  hashgcdlem  16127  coprimeprodsq  16147  coprimeprodsq2  16148  pythagtriplem3  16157  pcdvdsb  16207  pcgcd1  16215  dvdsprmpweq  16222  pcbc  16238  0ram  16358  ramz2  16362  ramub1lem1  16364  mremre  16877  mrieqv2d  16912  lubun  17735  isnsgrp  17907  issubmnd  17940  gsumccatOLD  18007  frmdss2  18030  submefmnd  18062  sgrp2rid2ex  18094  mulgnn0p1  18241  mulgnnsubcl  18242  mulgneg  18248  mulgdirlem  18260  nmzsubg  18319  ghmmulg  18372  pmtrfv  18582  pmtrmvd  18586  pmtrfb  18595  odmodnn0  18670  oddvdsnn0  18674  odnncl  18675  odmod  18676  oddvds  18677  odeq  18680  odmulgid  18683  odmulg  18685  odmulgeq  18686  odbezout  18687  odf1o1  18699  odf1o2  18700  odngen  18704  odcau  18731  pgpssslw  18741  fislw  18752  lsmless1x  18771  lsmless2x  18772  lsmsubm  18780  lsmmod  18803  lsmmod2  18804  efgsfo  18867  cntzcmn  18962  odadd1  18970  odadd2  18971  odadd  18972  lsmcomx  18978  prdscmnd  18983  gsumconst  19056  ring1eq0  19342  cntzsubr  19570  isabvd  19593  rmodislmod  19704  lspss  19758  0lmhm  19814  reslmhm2  19827  pwssplit0  19832  pwssplit1  19833  lbspss  19856  lspfixed  19902  lsmcv  19915  lspsnat  19919  issubassa  20100  aspss  20108  coe1subfv  20436  coe1tm  20443  xrsdsreclblem  20593  obselocv  20874  frlmsplit2  20919  frlmsslss2  20921  frlmup4  20947  lindff1  20966  lsslindf  20976  lsslinds  20977  islindf4  20984  mpomatmul  21057  mamutpos  21069  submaval  21192  mdetdiag  21210  mdetunilem1  21223  mdetunilem3  21225  mdetunilem9  21231  mdetmul  21234  maducoeval2  21251  madurid  21255  minmar1val  21259  cramer  21302  cpmatel2  21323  m2cpm  21351  decpmatmul  21382  pmatcollpw1lem2  21385  pmatcollpw1  21386  pmatcollpw2lem  21387  pm2mpcl  21407  mply1topmatcl  21415  mp2pm2mplem2  21417  mp2pm2mplem4  21419  pm2mpghmlem2  21422  pm2mpghmlem1  21423  cayhamlem2  21494  neiint  21714  topssnei  21734  cnrest2  21896  cnprest2  21900  cnt0  21956  cnt1  21960  cnhaus  21964  cncmp  22002  fiuncmp  22014  sscmp  22015  hauscmp  22017  cnconn  22032  unconn  22039  comppfsc  22142  kgen2ss  22165  ptpjopn  22222  ptrescn  22249  qtopss  22325  kqfvima  22340  r0cld  22348  cmphaushmeo  22410  fbssint  22448  fbasrn  22494  filuni  22495  ufilmax  22517  fin1aufil  22542  fmf  22555  fmss  22556  rnelfmlem  22562  rnelfm  22563  fmufil  22569  fmco  22571  flimss2  22582  flimss1  22583  flimrest  22593  cnpflf2  22610  cnpflf  22611  flfcnp  22614  lmflf  22615  supnfcls  22630  fclsss1  22632  fclsss2  22633  cnpfcfi  22650  subgntr  22717  opnsubg  22718  cldsubg  22721  ustuqtop1  22852  ucncn  22896  bldisj  23010  blgt0  23011  bl2in  23012  blss2ps  23015  blss2  23016  xbln0  23026  blssps  23036  blss  23037  lpbl  23115  blcld  23117  blcls  23118  stdbdmopn  23130  metcnp2  23154  txmetcnp  23159  blval2  23174  restmetu  23182  nmoix  23340  nmoi2  23341  nmoeq0  23347  nmotri  23350  metdsge  23459  metds0  23460  metdseq0  23464  icoopnst  23545  iccpnfhmeo  23551  xrhmeo  23552  nmhmcn  23726  cphsqrtcl2  23792  cphsqrtcl3  23793  fmcfil  23877  bcthlem5  23933  cmetcusp1  23958  cssbn  23980  pjth  24044  ovolunnul  24103  volun  24148  voliunlem2  24154  itg2const  24343  iblconst  24420  itgconst  24421  limcvallem  24471  dvcnp2  24519  dvcn  24520  deg1mul3le  24712  deg1tmle  24713  ig1pdvds  24772  coe11  24845  dgrmulc  24863  dvply1  24875  aaliou2  24931  efcvx  25039  tanord  25124  logdivlti  25205  logccv  25248  recxpcl  25260  cxplea  25281  cxple2a  25284  ang180  25394  isosctrlem2  25399  cxp2lim  25556  amgm  25570  muval1  25712  dvdssqf  25717  mumullem2  25759  bcmono  25855  lgsneg  25899  lgsmod  25901  lgsdirprm  25909  lgsdir  25910  lgsdi  25912  brbtwn2  26693  colinearalglem1  26694  colinearalg  26698  axcgrtr  26703  axcontlem2  26753  upgrewlkle2  27390  wlksoneq1eq2  27448  crctcshwlkn0lem5  27594  wspthsnwspthsnon  27697  lppthon  27932  upgriseupth  27988  4cyclusnfrgr  28073  numclwwlk1lem2foa  28135  numclwwlk5  28169  nvmul0or  28429  shless  29138  shlej1  29139  pjspansn  29356  kbmul  29734  homco2  29756  kbass2  29896  fnpreimac  30418  padct  30457  eliccelico  30502  elicoelioo  30503  iocinioc2  30504  difioo  30507  swrdrn2  30630  swrdrn3  30631  xrge0npcan  30683  isarchi2  30816  archiabl  30829  lindssn  30941  ssmxidl  30981  mdetlap1  31093  pstmfval  31138  fmcncfil  31176  zrhnm  31212  qqhnm  31233  nexple  31270  volfiniune  31491  omsmeas  31583  eulerpartlemb  31628  probinc  31681  cndprob01  31695  signswmnd  31829  cvmsss2  32523  dvdspw  32984  funsseq  33013  frpomin  33080  frrlem10  33134  fprlem1  33139  sltres  33171  nolt02olem  33200  nolt02o  33201  nosupbnd1lem1  33210  nosupbnd1lem4  33213  nosupbnd1lem5  33214  nosupbnd1lem6  33215  cgrtriv  33465  5segofs  33469  btwntriv2  33475  btwnxfr  33519  segcon2  33568  brsegle2  33572  seglelin  33579  outsideofeu  33594  lindsenlbs  34889  mblfinlem2  34932  blbnd  35067  rrndstprj2  35111  zerdivemp1x  35227  lsmsat  36146  lsatfixedN  36147  lssat  36154  lkrlsp  36240  lshpkrlem4  36251  cvrcon3b  36415  leat3  36433  atlen0  36448  atnle  36455  atlatmstc  36457  atlatle  36458  cvlcvr1  36477  cvlsupr2  36481  hlsupr2  36525  hlrelat2  36541  cvrexchlem  36557  cvratlem  36559  lnnat  36565  atexchcvrN  36578  1cvratlt  36612  1cvrjat  36613  3atlem3  36623  3atlem7  36627  llni2  36650  atcvrlln2  36657  llnexatN  36659  llncmp  36660  2llnmat  36662  2at0mat0  36663  2atnelpln  36682  llncvrlpln2  36695  2lplnmN  36697  2llnmj  36698  lplncmp  36700  lplnexatN  36701  2llnjaN  36704  lvoli3  36715  islvol2aN  36730  4atlem3a  36735  4atlem4a  36737  4atlem4b  36738  4atlem11  36747  4atlem12  36750  lplncvrlvol2  36753  lvolcmp  36755  2lplnmj  36760  islinei  36878  linepmap  36913  lneq2at  36916  2llnma3r  36926  elpaddn0  36938  elpaddatriN  36941  elpaddat  36942  paddcom  36951  paddss1  36955  paddss2  36956  paddasslem6  36963  paddasslem7  36964  paddasslem10  36967  paddasslem15  36972  pmodlem2  36985  pmodl42N  36989  pmapjoin  36990  atmod1i1m  36996  llnmod1i2  36998  llnexchb2lem  37006  polcon2bN  37058  pclfinclN  37088  poml4N  37091  poml6N  37093  osumcllem11N  37104  osumclN  37105  pmapojoinN  37106  pexmidlem2N  37109  pexmidlem3N  37110  pexmidlem4N  37111  pexmidlem6N  37113  pexmidlem7N  37114  pl42lem2N  37118  pl42lem3N  37119  pl42lem4N  37120  pl42N  37121  lhpexle3lem  37149  lhpmcvr3  37163  lhp2at0nle  37173  lhprelat3N  37178  lauteq  37233  lautco  37235  ltrncoidN  37266  ltrneq2  37286  ltrnnidn  37312  ltrnideq  37313  trlnle  37324  cdlemc  37335  cdlemd4  37339  cdlemd5  37340  cdlemd9  37344  cdlemd  37345  ltrneq3  37346  cdlemefrs29pre00  37533  cdlemefrs29cpre1  37536  cdlemefrs29clN  37537  cdlemefrs32fva  37538  cdlemefr29exN  37540  cdlemefr27cl  37541  cdlemefs27cl  37551  cdlemefs32sn1aw  37552  cdleme32fva  37575  cdleme32d  37582  cdleme32f  37584  cdleme32le  37585  cdleme40n  37606  cdleme41snaw  37614  cdleme17d3  37634  cdleme48fvg  37638  cdlemeg46fvcl  37644  cdlemeg46fgN  37672  cdleme48fgv  37676  ltrniotavalbN  37722  cdlemb3  37744  cdlemg15  37794  cdlemg17dN  37801  trlco  37865  cdlemg44b  37870  ltrncom  37876  trljco  37878  tendococl  37910  tendoplcl  37919  tendoplcom  37920  tendotr  37968  cdlemk36  38051  cdlemk35s-id  38076  cdlemk39s-id  38078  cdlemk19x  38081  cdlemk53b  38094  cdlemk55  38099  cdlemk35u  38102  cdlemk55u  38104  cdlemk39u  38106  cdlemk19u  38108  cdlemk56  38109  tendoex  38113  cdleml5N  38118  dihord2pre  38363  dihord6apre  38394  dihord5b  38397  dihord5apre  38400  dihord  38402  dihmeetlem1N  38428  dihmeetlem2N  38437  dihglbcpreN  38438  dihmeetbN  38441  dihmeetlem4preN  38444  dihmeetlem5  38446  dihmeetlem6  38447  dihmeetlem7N  38448  dihmeetlem10N  38454  dihmeetlem11N  38455  dihmeetlem12N  38456  dihmeetlem13N  38457  dihmeetlem15N  38459  dihmeetlem17N  38461  dihmeetlem18N  38462  dihmeetlem19N  38463  dihmeetALTN  38465  dih1dimatlem0  38466  dihlspsnssN  38470  dvh3dim2  38586  resubcan2  39225  mzpsubst  39352  diophrw  39363  eldioph2lem1  39364  rencldnfi  39425  pellexlem2  39434  pellqrexplicit  39481  infmrgelbi  39482  rmxycomplete  39521  congadd  39570  acongeq  39587  jm2.19  39597  jm2.22  39599  jm2.20nn  39601  jm2.25lem1  39602  jm2.27  39612  jm3.1  39624  lmhmlnmsplit  39694  pwssplit4  39696  hbtlem2  39731  dgraa0p  39756  idomrootle  39802  proot1hash  39807  iocunico  39824  relexpxpmin  40069  brtrclfv2  40079  ntrclsk3  40427  grur1cld  40575  ismnu  40604  suprnmpt  41437  wessf1ornlem  41452  choicefi  41470  supxrgere  41608  supxrgelem  41612  supxrge  41613  infleinflem2  41646  snunioo1  41795  iccintsng  41806  fmul01  41868  lptre2pt  41928  0ellimcdiv  41937  fnlimfvre  41962  limsupmnfuzlem  42014  climisp  42034  limsupgtlem  42065  ibliccsinexp  42243  iblioosinexp  42245  volioc  42264  iblspltprt  42265  stoweidlem20  42312  stoweidlem22  42314  stoweidlem34  42326  stoweidlem44  42336  stoweidlem60  42352  wallispilem3  42359  fourierdlem42  42441  fourierdlem51  42449  fourierdlem54  42452  fourierdlem87  42485  fourierdlem97  42495  ioorrnopnlem  42596  sge0seq  42735  hoicvr  42837  imasetpreimafvbijlemfv  43569  lincresunit3lem3  44536  lindssnlvec  44548  rrx2linesl  44737  line2  44746  itsclc0lem3  44752  itsclc0yqsollem1  44756  itscnhlc0xyqsol  44759  itschlc0xyqsol1  44760  itsclc0  44765  itscnhlinecirc02plem2  44777  itscnhlinecirc02plem3  44778