Theorem simpl3 1190

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  simpl13  1247  simpl23  1250  simpl33  1253  simp1l3  1265  simp2l3  1271  simp3l3  1277  3anandirs  1469  2nreu  4349  f1prex  7018  fcofo  7022  soisores  7059  weniso  7086  knatar  7089  ofmpteq  7408  funelss  7728  smorndom  7988  nnmord  8241  nnmword  8242  difsnen  8582  mapunen  8670  ac6sfi  8746  fipreima  8814  wemaplem2  8995  wemapso2lem  9000  en2eqpr  9418  indcardi  9452  acndom  9462  fodomfi2  9471  infmap2  9629  cflim2  9674  coftr  9684  infpssrlem4  9717  fin23lem11  9728  fincssdom  9734  isf32lem9  9772  fin1a2lem9  9819  gchpwdom  10081  gruima  10213  prpssnq  10401  distrlem4pr  10437  dedekind  10792  addcan  10813  addcan2  10814  divmulass  11310  supmul1  11597  uzsupss  12328  xaddass  12630  xleadd1a  12634  xlesubadd  12644  xmulasslem3  12667  xmulass  12668  xadddilem  12675  xadddi  12676  ixxun  12742  icoshftf1o  12852  snunioc  12858  difelfzle  13015  fzo1fzo0n0  13083  ssfzoulel  13126  modmuladd  13276  modifeq2int  13296  modaddmulmod  13301  modsubdir  13303  ltexp2a  13526  leexp2  13531  ltexp2r  13533  exple1  13536  expnlbnd2  13591  mulsubdivbinom2  13618  hashtpg  13839  ccatass  13933  ccatopth  14069  pfxccatin12lem2a  14080  pfxccat3  14087  cshinj  14164  2cshw  14166  s2f1o  14269  limsupgre  14830  addcn2  14942  mulcn2  14944  binomrisefac  15388  bpolydif  15401  dvdsmodexp  15607  modmulconst  15633  dvdsmod  15670  sadass  15810  gcdass  15885  rplpwr  15897  rppwr  15898  rpmulgcd2  15990  rpdvds  15994  rpexp  16054  prmdiveq  16113  hashgcdlem  16115  coprimeprodsq  16135  coprimeprodsq2  16136  pythagtriplem3  16145  pcdvdsb  16195  pcgcd1  16203  dvdsprmpweq  16210  pcbc  16226  0ram  16346  ramz2  16350  ramub1lem1  16352  mremre  16867  mrieqv2d  16902  lubun  17725  isnsgrp  17897  issubmnd  17930  gsumccatOLD  17997  frmdss2  18020  submefmnd  18052  sgrp2rid2ex  18084  mulgnn0p1  18231  mulgnnsubcl  18232  mulgneg  18238  mulgdirlem  18250  nmzsubg  18309  ghmmulg  18362  pmtrfv  18572  pmtrmvd  18576  pmtrfb  18585  odmodnn0  18660  oddvdsnn0  18664  odnncl  18665  odmod  18666  oddvds  18667  odeq  18670  odmulgid  18673  odmulg  18675  odmulgeq  18676  odbezout  18677  odf1o1  18689  odf1o2  18690  odngen  18694  odcau  18721  pgpssslw  18731  fislw  18742  lsmless1x  18761  lsmless2x  18762  lsmsubm  18770  lsmmod  18793  lsmmod2  18794  efgsfo  18857  cntzcmn  18953  odadd1  18961  odadd2  18962  odadd  18963  lsmcomx  18969  prdscmnd  18974  gsumconst  19047  ring1eq0  19336  cntzsubr  19561  isabvd  19584  rmodislmod  19695  lspss  19749  0lmhm  19805  reslmhm2  19818  pwssplit0  19823  pwssplit1  19824  lbspss  19847  lspfixed  19893  lsmcv  19906  lspsnat  19910  xrsdsreclblem  20137  obselocv  20417  frlmsplit2  20462  frlmsslss2  20464  frlmup4  20490  lindff1  20509  lsslindf  20519  lsslinds  20520  islindf4  20527  issubassa  20555  aspss  20563  coe1subfv  20895  coe1tm  20902  mpomatmul  21051  mamutpos  21063  submaval  21186  mdetdiag  21204  mdetunilem1  21217  mdetunilem3  21219  mdetunilem9  21225  mdetmul  21228  maducoeval2  21245  madurid  21249  minmar1val  21253  cramer  21296  cpmatel2  21318  m2cpm  21346  decpmatmul  21377  pmatcollpw1lem2  21380  pmatcollpw1  21381  pmatcollpw2lem  21382  pm2mpcl  21402  mply1topmatcl  21410  mp2pm2mplem2  21412  mp2pm2mplem4  21414  pm2mpghmlem2  21417  pm2mpghmlem1  21418  cayhamlem2  21489  neiint  21709  topssnei  21729  cnrest2  21891  cnprest2  21895  cnt0  21951  cnt1  21955  cnhaus  21959  cncmp  21997  fiuncmp  22009  sscmp  22010  hauscmp  22012  cnconn  22027  unconn  22034  comppfsc  22137  kgen2ss  22160  ptpjopn  22217  ptrescn  22244  qtopss  22320  kqfvima  22335  r0cld  22343  cmphaushmeo  22405  fbssint  22443  fbasrn  22489  filuni  22490  ufilmax  22512  fin1aufil  22537  fmf  22550  fmss  22551  rnelfmlem  22557  rnelfm  22558  fmufil  22564  fmco  22566  flimss2  22577  flimss1  22578  flimrest  22588  cnpflf2  22605  cnpflf  22606  flfcnp  22609  lmflf  22610  supnfcls  22625  fclsss1  22627  fclsss2  22628  cnpfcfi  22645  subgntr  22712  opnsubg  22713  cldsubg  22716  ustuqtop1  22847  ucncn  22891  bldisj  23005  blgt0  23006  bl2in  23007  blss2ps  23010  blss2  23011  xbln0  23021  blssps  23031  blss  23032  lpbl  23110  blcld  23112  blcls  23113  stdbdmopn  23125  metcnp2  23149  txmetcnp  23154  blval2  23169  restmetu  23177  nmoix  23335  nmoi2  23336  nmoeq0  23342  nmotri  23345  metdsge  23454  metds0  23455  metdseq0  23459  icoopnst  23544  iccpnfhmeo  23550  xrhmeo  23551  nmhmcn  23725  cphsqrtcl2  23791  cphsqrtcl3  23792  fmcfil  23876  bcthlem5  23932  cmetcusp1  23957  cssbn  23979  pjth  24043  ovolunnul  24104  volun  24149  voliunlem2  24155  itg2const  24344  iblconst  24421  itgconst  24422  limcvallem  24474  dvcnp2  24523  dvcn  24524  deg1mul3le  24717  deg1tmle  24718  ig1pdvds  24777  coe11  24850  dgrmulc  24868  dvply1  24880  aaliou2  24936  efcvx  25044  tanord  25130  logdivlti  25211  logccv  25254  recxpcl  25266  cxplea  25287  cxple2a  25290  ang180  25400  isosctrlem2  25405  cxp2lim  25562  amgm  25576  muval1  25718  dvdssqf  25723  mumullem2  25765  bcmono  25861  lgsneg  25905  lgsmod  25907  lgsdirprm  25915  lgsdir  25916  lgsdi  25918  brbtwn2  26699  colinearalglem1  26700  colinearalg  26704  axcgrtr  26709  axcontlem2  26759  upgrewlkle2  27396  wlksoneq1eq2  27454  crctcshwlkn0lem5  27600  wspthsnwspthsnon  27702  lppthon  27936  upgriseupth  27992  4cyclusnfrgr  28077  numclwwlk1lem2foa  28139  numclwwlk5  28173  nvmul0or  28433  shless  29142  shlej1  29143  pjspansn  29360  kbmul  29738  homco2  29760  kbass2  29900  fnpreimac  30434  padct  30481  eliccelico  30526  elicoelioo  30527  iocinioc2  30528  difioo  30531  swrdrn2  30654  swrdrn3  30655  xrge0npcan  30728  isarchi2  30864  archiabl  30877  pidlnz  30991  lindssn  30993  ssmxidl  31050  mdetlap1  31179  zarclsiin  31224  pstmfval  31249  fmcncfil  31284  zrhnm  31320  qqhnm  31341  nexple  31378  volfiniune  31599  omsmeas  31691  eulerpartlemb  31736  probinc  31789  cndprob01  31803  signswmnd  31937  cvmsss2  32634  dvdspw  33095  funsseq  33124  frpomin  33191  frrlem10  33245  fprlem1  33250  sltres  33282  nolt02olem  33311  nolt02o  33312  nosupbnd1lem1  33321  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd1lem6  33326  cgrtriv  33576  5segofs  33580  btwntriv2  33586  btwnxfr  33630  segcon2  33679  brsegle2  33683  seglelin  33690  outsideofeu  33705  lindsenlbs  35052  mblfinlem2  35095  blbnd  35225  rrndstprj2  35269  zerdivemp1x  35385  lsmsat  36304  lsatfixedN  36305  lssat  36312  lkrlsp  36398  lshpkrlem4  36409  cvrcon3b  36573  leat3  36591  atlen0  36606  atnle  36613  atlatmstc  36615  atlatle  36616  cvlcvr1  36635  cvlsupr2  36639  hlsupr2  36683  hlrelat2  36699  cvrexchlem  36715  cvratlem  36717  lnnat  36723  atexchcvrN  36736  1cvratlt  36770  1cvrjat  36771  3atlem3  36781  3atlem7  36785  llni2  36808  atcvrlln2  36815  llnexatN  36817  llncmp  36818  2llnmat  36820  2at0mat0  36821  2atnelpln  36840  llncvrlpln2  36853  2lplnmN  36855  2llnmj  36856  lplncmp  36858  lplnexatN  36859  2llnjaN  36862  lvoli3  36873  islvol2aN  36888  4atlem3a  36893  4atlem4a  36895  4atlem4b  36896  4atlem11  36905  4atlem12  36908  lplncvrlvol2  36911  lvolcmp  36913  2lplnmj  36918  islinei  37036  linepmap  37071  lneq2at  37074  2llnma3r  37084  elpaddn0  37096  elpaddatriN  37099  elpaddat  37100  paddcom  37109  paddss1  37113  paddss2  37114  paddasslem6  37121  paddasslem7  37122  paddasslem10  37125  paddasslem15  37130  pmodlem2  37143  pmodl42N  37147  pmapjoin  37148  atmod1i1m  37154  llnmod1i2  37156  llnexchb2lem  37164  polcon2bN  37216  pclfinclN  37246  poml4N  37249  poml6N  37251  osumcllem11N  37262  osumclN  37263  pmapojoinN  37264  pexmidlem2N  37267  pexmidlem3N  37268  pexmidlem4N  37269  pexmidlem6N  37271  pexmidlem7N  37272  pl42lem2N  37276  pl42lem3N  37277  pl42lem4N  37278  pl42N  37279  lhpexle3lem  37307  lhpmcvr3  37321  lhp2at0nle  37331  lhprelat3N  37336  lauteq  37391  lautco  37393  ltrncoidN  37424  ltrneq2  37444  ltrnnidn  37470  ltrnideq  37471  trlnle  37482  cdlemc  37493  cdlemd4  37497  cdlemd5  37498  cdlemd9  37502  cdlemd  37503  ltrneq3  37504  cdlemefrs29pre00  37691  cdlemefrs29cpre1  37694  cdlemefrs29clN  37695  cdlemefrs32fva  37696  cdlemefr29exN  37698  cdlemefr27cl  37699  cdlemefs27cl  37709  cdlemefs32sn1aw  37710  cdleme32fva  37733  cdleme32d  37740  cdleme32f  37742  cdleme32le  37743  cdleme40n  37764  cdleme41snaw  37772  cdleme17d3  37792  cdleme48fvg  37796  cdlemeg46fvcl  37802  cdlemeg46fgN  37830  cdleme48fgv  37834  ltrniotavalbN  37880  cdlemb3  37902  cdlemg15  37952  cdlemg17dN  37959  trlco  38023  cdlemg44b  38028  ltrncom  38034  trljco  38036  tendococl  38068  tendoplcl  38077  tendoplcom  38078  tendotr  38126  cdlemk36  38209  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk19x  38239  cdlemk53b  38252  cdlemk55  38257  cdlemk35u  38260  cdlemk55u  38262  cdlemk39u  38264  cdlemk19u  38266  cdlemk56  38267  tendoex  38271  cdleml5N  38276  dihord2pre  38521  dihord6apre  38552  dihord5b  38555  dihord5apre  38558  dihord  38560  dihmeetlem1N  38586  dihmeetlem2N  38595  dihglbcpreN  38596  dihmeetbN  38599  dihmeetlem4preN  38602  dihmeetlem5  38604  dihmeetlem6  38605  dihmeetlem7N  38606  dihmeetlem10N  38612  dihmeetlem11N  38613  dihmeetlem12N  38614  dihmeetlem13N  38615  dihmeetlem15N  38617  dihmeetlem17N  38619  dihmeetlem18N  38620  dihmeetlem19N  38621  dihmeetALTN  38623  dih1dimatlem0  38624  dihlspsnssN  38628  dvh3dim2  38744  resubcan2  39526  mzpsubst  39689  diophrw  39700  eldioph2lem1  39701  rencldnfi  39762  pellexlem2  39771  pellqrexplicit  39818  infmrgelbi  39819  rmxycomplete  39858  congadd  39907  acongeq  39924  jm2.19  39934  jm2.22  39936  jm2.20nn  39938  jm2.25lem1  39939  jm2.27  39949  jm3.1  39961  lmhmlnmsplit  40031  pwssplit4  40033  hbtlem2  40068  dgraa0p  40093  idomrootle  40139  proot1hash  40144  iocunico  40161  relexpxpmin  40418  brtrclfv2  40428  ntrclsk3  40773  grur1cld  40940  ismnu  40969  suprnmpt  41798  wessf1ornlem  41811  choicefi  41829  supxrgere  41965  supxrgelem  41969  supxrge  41970  infleinflem2  42003  snunioo1  42149  iccintsng  42160  fmul01  42222  lptre2pt  42282  0ellimcdiv  42291  fnlimfvre  42316  limsupmnfuzlem  42368  climisp  42388  limsupgtlem  42419  ibliccsinexp  42593  iblioosinexp  42595  volioc  42614  iblspltprt  42615  stoweidlem20  42662  stoweidlem22  42664  stoweidlem34  42676  stoweidlem44  42686  stoweidlem60  42702  wallispilem3  42709  fourierdlem42  42791  fourierdlem51  42799  fourierdlem54  42802  fourierdlem87  42835  fourierdlem97  42845  ioorrnopnlem  42946  sge0seq  43085  hoicvr  43187  imasetpreimafvbijlemfv  43919  fprmappr  44747  lincresunit3lem3  44883  lindssnlvec  44895  rrx2linesl  45157  line2  45166  itsclc0lem3  45172  itsclc0yqsollem1  45176  itscnhlc0xyqsol  45179  itschlc0xyqsol1  45180  itsclc0  45185  itscnhlinecirc02plem2  45197  itscnhlinecirc02plem3  45198