Theorem simpl3 1212

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl13  1269  simpl23  1272  simpl33  1275  simp1l3  1287  simp2l3  1293  simp3l3  1299  3anandirs  1501  2nreu  4402  predtrss  6318  frpomin  6336  f1prex  7284  fcofo  7288  soisores  7327  weniso  7356  knatar  7359  ofmpteq  7705  funelss  8047  frrlem10  8297  fprlem1  8302  smocdmdom  8360  nnmord  8625  nnmword  8626  naddasslem1  8688  naddasslem2  8689  difsnen  9062  mapunen  9149  ac6sfi  9259  fipreima  9331  wemaplem2  9525  wemapso2lem  9530  ttrclselem2  9711  en2eqpr  10067  indcardi  10101  acndom  10111  fodomfi2  10120  infmap2  10276  cflim2  10322  coftr  10332  infpssrlem4  10365  fin23lem11  10376  fincssdom  10382  isf32lem9  10420  fin1a2lem9  10467  gchpwdom  10736  gruima  10868  prpssnq  11056  distrlem4pr  11092  dedekind  11454  addcan  11475  addcan2  11476  divmulass  11978  supmul1  12267  uzsupss  13048  xaddass  13360  xleadd1a  13364  xlesubadd  13374  xmulasslem3  13397  xmulass  13398  xadddilem  13405  xadddi  13406  ixxun  13473  icoshftf1o  13586  snunioc  13592  difelfzle  13755  fzo1fzo0n0  13830  ssfzoulel  13875  modmuladd  14036  modifeq2int  14056  modaddmulmod  14061  modsubdir  14063  ltexp2a  14289  leexp2  14294  ltexp2r  14296  exple1  14300  expnlbnd2  14358  mulsubdivbinom2  14386  hashtpg  14610  ccatass  14714  swrdrn3  14782  ccatopth  14845  pfxccatin12lem2a  14856  pfxccat3  14863  cshinj  14942  2cshw  14944  s2f1o  15047  limsupgre  15628  addcn2  15741  mulcn2  15743  binomrisefac  16188  bpolydif  16201  dvdsmodexp  16410  modmulconst  16438  dvdsexp2im  16477  dvdsmod  16479  sadass  16621  gcdass  16700  rplpwr  16712  dvdsexpnn  16720  rpmulgcd2  16811  rpdvds  16815  rpexp  16878  prmdiveq  16943  hashgcdlem  16945  coprimeprodsq  16966  coprimeprodsq2  16967  pythagtriplem3  16976  pcdvdsb  17027  pcgcd1  17035  dvdsprmpweq  17042  pcbc  17058  0ram  17178  ramz2  17182  ramub1lem1  17184  mremre  17754  mrieqv2d  17793  lubun  18669  isnsgrp  18892  issubmnd  18933  frmdss2  19039  submefmnd  19071  sgrp2rid2ex  19106  mulgnn0p1  19275  mulgnnsubcl  19276  mulgneg  19282  mulgdirlem  19295  nmzsubg  19355  ghmmulg  19422  pmtrfv  19646  pmtrmvd  19650  pmtrfb  19659  odmodnn0  19734  oddvdsnn0  19738  odnncl  19739  odmod  19740  oddvds  19741  odeq  19744  odmulgid  19748  odmulg  19750  odmulgeq  19751  odbezout  19752  odf1o1  19766  odf1o2  19767  odngen  19771  odcau  19798  pgpssslw  19808  fislw  19819  lsmless1x  19838  lsmless2x  19839  lsmsubm  19847  lsmmod  19869  lsmmod2  19870  efgsfo  19933  cntzcmn  20034  odadd1  20042  odadd2  20043  odadd  20044  lsmcomx  20050  prdscmnd  20055  gsumconst  20128  ring1eq0  20509  cntzsubrng  20799  cntzsubr  20838  isabvd  21049  rmodislmod  21185  lspss  21239  0lmhm  21295  reslmhm2  21308  pwssplit0  21313  pwssplit1  21314  lbspss  21337  lspfixed  21386  lsmcv  21399  lspsnat  21403  pidlnz  21508  2idlcpblrng  21545  cnfldfunALT  21673  xrsdsreclblem  21699  obselocv  22014  frlmsplit2  22059  frlmsslss2  22061  frlmup4  22087  lindff1  22106  lsslindf  22116  lsslinds  22117  islindf4  22124  lindsenlbs  22137  issubassa  22155  aspss  22164  coe1subfv  22565  coe1tm  22572  mpomatmul  22741  mamutpos  22753  submaval  22876  mdetdiag  22894  mdetunilem1  22907  mdetunilem3  22909  mdetunilem9  22915  mdetmul  22918  maducoeval2  22935  madurid  22939  minmar1val  22943  cramer  22989  cpmatel2  23011  m2cpm  23039  decpmatmul  23070  pmatcollpw1lem2  23073  pmatcollpw1  23074  pmatcollpw2lem  23075  pm2mpcl  23095  mply1topmatcl  23103  mp2pm2mplem2  23105  mp2pm2mplem4  23107  pm2mpghmlem2  23110  pm2mpghmlem1  23111  cayhamlem2  23182  neiint  23402  topssnei  23422  cnrest2  23584  cnprest2  23588  cnt0  23644  cnt1  23648  cnhaus  23652  cncmp  23690  fiuncmp  23702  sscmp  23703  hauscmp  23705  cnconn  23720  unconn  23727  comppfsc  23831  kgen2ss  23854  ptpjopn  23911  ptrescn  23938  qtopss  24014  kqfvima  24029  r0cld  24037  cmphaushmeo  24099  fbssint  24137  fbasrn  24183  filuni  24184  ufilmax  24206  fin1aufil  24231  fmf  24244  fmss  24245  rnelfmlem  24251  rnelfm  24252  fmufil  24258  fmco  24260  flimss2  24271  flimss1  24272  flimrest  24282  cnpflf2  24299  cnpflf  24300  flfcnp  24303  lmflf  24304  supnfcls  24319  fclsss1  24321  fclsss2  24322  cnpfcfi  24339  subgntr  24406  opnsubg  24407  cldsubg  24410  ustuqtop1  24540  ucncn  24583  bldisj  24697  blgt0  24698  bl2in  24699  blss2ps  24702  blss2  24703  xbln0  24713  blssps  24723  blss  24724  lpbl  24802  blcld  24804  blcls  24805  stdbdmopn  24817  metcnp2  24841  txmetcnp  24846  blval2  24861  restmetu  24869  nmoix  25028  nmoi2  25029  nmoeq0  25035  nmotri  25038  metdsge  25149  metds0  25150  metdseq0  25154  icoopnst  25240  iccpnfhmeo  25246  xrhmeo  25247  nmhmcn  25421  cphsqrtcl2  25487  cphsqrtcl3  25488  fmcfil  25573  bcthlem5  25629  cmetcusp1  25654  cssbn  25676  pjth  25740  ovolunnul  25801  volun  25846  voliunlem2  25852  itg2const  26041  iblconst  26118  itgconst  26119  limcvallem  26171  dvcnp2  26220  dvcn  26221  deg1mul3le  26415  deg1tmle  26416  idomrootle  26471  ig1pdvds  26478  coe11  26552  dgrmulc  26570  dvply1  26587  aaliou2  26649  efcvx  26758  tanord  26848  logdivlti  26930  logccv  26973  recxpcl  26985  cxplea  27006  cxple2a  27009  ang180  27124  isosctrlem2  27129  cxp2lim  27286  amgm  27300  muval1  27442  dvdssqf  27447  mumullem2  27489  bcmono  27586  lgsneg  27630  lgsmod  27632  lgsdirprm  27640  lgsdir  27641  lgsdi  27643  ltsres  28001  nolt02olem  28033  nolt02o  28034  nogt01o  28035  nosupbnd1lem1  28047  nosupbnd1lem4  28050  nosupbnd1lem5  28051  nosupbnd1lem6  28052  noinfbnd1lem1  28062  noinfbnd1lem4  28065  noinfbnd1lem6  28067  noinfbnd2  28070  noetainflem3  28078  ltslpss  28276  cofslts  28286  coinitslts  28287  cofcutrtime  28295  addsass  28373  addsdi  28523  mulsass  28534  ltmuls2  28539  norecdiv  28558  z12bdaylem  28852  brbtwn2  29465  colinearalglem1  29466  colinearalg  29470  axcgrtr  29475  axcontlem2  29525  upgrewlkle2  30169  wlksoneq1eq2  30225  crctcshwlkn0lem5  30385  wspthsnwspthsnon  30487  lppthon  30724  upgriseupth  30790  4cyclusnfrgr  30875  numclwwlk1lem2foa  30937  numclwwlk5  30971  nvmul0or  31234  shless  31943  shlej1  31944  pjspansn  32161  kbmul  32539  homco2  32561  kbass2  32701  fnpreimac  33246  padct  33292  eliccelico  33351  elicoelioo  33352  iocinioc2  33353  difioo  33356  nexple  33406  swrdrn2  33499  xrge0npcan  33563  isarchi2  33728  archiabl  33741  lindssn  33915  ssmxidl  33981  mdetlap1  34440  zarclsiin  34485  pstmfval  34510  fmcncfil  34545  zrhnm  34581  qqhnm  34604  volfiniune  34845  omsmeas  34938  eulerpartlemb  34983  probinc  35036  cndprob01  35050  signswmnd  35169  cvmsss2  36008  funsseq  36502  cgrtriv  36737  5segofs  36741  btwntriv2  36747  btwnxfr  36791  segcon2  36840  brsegle2  36844  seglelin  36851  outsideofeu  36866  nmulss1  36933  ltnmul  36935  nmulle  36936  ltnadd  36937  naddle  36938  nadddi  36943  weiunpo  37223  weiunfr  37225  weiunse  37226  mblfinlem2  38544  blbnd  38689  rrndstprj2  38733  zerdivemp1x  38849  lsmsat  40033  lsatfixedN  40034  lssat  40041  lkrlsp  40127  lshpkrlem4  40138  cvrcon3b  40302  leat3  40320  atlen0  40335  atnle  40342  atlatmstc  40344  atlatle  40345  cvlcvr1  40364  cvlsupr2  40368  hlsupr2  40412  hlrelat2  40428  cvrexchlem  40444  cvratlem  40446  lnnat  40452  atexchcvrN  40465  1cvratlt  40499  1cvrjat  40500  3atlem3  40510  3atlem7  40514  llni2  40537  atcvrlln2  40544  llnexatN  40546  llncmp  40547  2llnmat  40549  2at0mat0  40550  2atnelpln  40569  llncvrlpln2  40582  2lplnmN  40584  2llnmj  40585  lplncmp  40587  lplnexatN  40588  2llnjaN  40591  lvoli3  40602  islvol2aN  40617  4atlem3a  40622  4atlem4a  40624  4atlem4b  40625  4atlem11  40634  4atlem12  40637  lplncvrlvol2  40640  lvolcmp  40642  2lplnmj  40647  islinei  40765  linepmap  40800  lneq2at  40803  2llnma3r  40813  elpaddn0  40825  elpaddatriN  40828  elpaddat  40829  paddcom  40838  paddss1  40842  paddss2  40843  paddasslem6  40850  paddasslem7  40851  paddasslem10  40854  paddasslem15  40859  pmodlem2  40872  pmodl42N  40876  pmapjoin  40877  atmod1i1m  40883  llnmod1i2  40885  llnexchb2lem  40893  polcon2bN  40945  pclfinclN  40975  poml4N  40978  poml6N  40980  osumcllem11N  40991  osumclN  40992  pmapojoinN  40993  pexmidlem2N  40996  pexmidlem3N  40997  pexmidlem4N  40998  pexmidlem6N  41000  pexmidlem7N  41001  pl42lem2N  41005  pl42lem3N  41006  pl42lem4N  41007  pl42N  41008  lhpexle3lem  41036  lhpmcvr3  41050  lhp2at0nle  41060  lhprelat3N  41065  lauteq  41120  lautco  41122  ltrncoidN  41153  ltrneq2  41173  ltrnnidn  41199  ltrnideq  41200  trlnle  41211  cdlemc  41222  cdlemd4  41226  cdlemd5  41227  cdlemd9  41231  cdlemd  41232  ltrneq3  41233  cdlemefrs29pre00  41420  cdlemefrs29cpre1  41423  cdlemefrs29clN  41424  cdlemefrs32fva  41425  cdlemefr29exN  41427  cdlemefr27cl  41428  cdlemefs27cl  41438  cdlemefs32sn1aw  41439  cdleme32fva  41462  cdleme32d  41469  cdleme32f  41471  cdleme32le  41472  cdleme40n  41493  cdleme41snaw  41501  cdleme17d3  41521  cdleme48fvg  41525  cdlemeg46fvcl  41531  cdlemeg46fgN  41559  cdleme48fgv  41563  ltrniotavalbN  41609  cdlemb3  41631  cdlemg15  41681  cdlemg17dN  41688  trlco  41752  cdlemg44b  41757  ltrncom  41763  trljco  41765  tendococl  41797  tendoplcl  41806  tendoplcom  41807  tendotr  41855  cdlemk36  41938  cdlemk35s-id  41963  cdlemk39s-id  41965  cdlemk19x  41968  cdlemk53b  41981  cdlemk55  41986  cdlemk35u  41989  cdlemk55u  41991  cdlemk39u  41993  cdlemk19u  41995  cdlemk56  41996  tendoex  42000  cdleml5N  42005  dihord2pre  42250  dihord6apre  42281  dihord5b  42284  dihord5apre  42287  dihord  42289  dihmeetlem1N  42315  dihmeetlem2N  42324  dihglbcpreN  42325  dihmeetbN  42328  dihmeetlem4preN  42331  dihmeetlem5  42333  dihmeetlem6  42334  dihmeetlem7N  42335  dihmeetlem10N  42341  dihmeetlem11N  42342  dihmeetlem12N  42343  dihmeetlem13N  42344  dihmeetlem15N  42346  dihmeetlem17N  42348  dihmeetlem18N  42349  dihmeetlem19N  42350  dihmeetALTN  42352  dih1dimatlem0  42353  dihlspsnssN  42357  dvh3dim2  42473  sticksstones1  43164  sticksstones2  43165  sticksstones12  43176  aks6d1c6isolem1  43192  resubcan2  43407  mzpsubst  43712  diophrw  43723  eldioph2lem1  43724  rencldnfi  43781  pellexlem2  43790  pellqrexplicit  43837  infmrgelbi  43838  rmxycomplete  43877  congadd  43926  acongeq  43943  jm2.19  43953  jm2.22  43955  jm2.20nn  43957  jm2.25lem1  43958  jm2.27  43968  jm3.1  43980  lmhmlnmsplit  44047  pwssplit4  44049  hbtlem2  44084  dgraa0p  44109  proot1hash  44155  iocunico  44171  cantnf2  44285  dflim5  44289  omcl2  44293  tfsconcatrn  44302  nadd2rabex  44346  relexpxpmin  44676  brtrclfv2  44686  ntrclsk3  45029  grur1cld  45189  ismnu  45204  suprnmpt  46132  wessf1ornlem  46143  choicefi  46157  supxrgere  46289  supxrgelem  46293  supxrge  46294  infleinflem2  46326  snunioo1  46468  iccintsng  46479  fmul01  46536  lptre2pt  46594  0ellimcdiv  46603  fnlimfvre  46628  limsupmnfuzlem  46680  climisp  46700  limsupgtlem  46731  ibliccsinexp  46905  iblioosinexp  46907  volioc  46926  iblspltprt  46927  stoweidlem20  46974  stoweidlem22  46976  stoweidlem34  46988  stoweidlem44  46998  stoweidlem60  47014  wallispilem3  47021  fourierdlem42  47103  fourierdlem51  47111  fourierdlem54  47114  fourierdlem87  47147  fourierdlem97  47157  ioorrnopnlem  47258  sge0seq  47400  hoicvr  47502  fsupdm  47796  finfdm  47800  3f1oss1  48089  funfocofob  48092  imasetpreimafvbijlemfv  48428  uhgrimisgrgric  48973  uhgrimgrlim  49029  fprmappr  49401  lincresunit3lem3  49530  lindssnlvec  49542  rrx2linesl  49799  line2  49808  itsclc0lem3  49814  itsclc0yqsollem1  49818  itscnhlc0xyqsol  49821  itschlc0xyqsol1  49822  itsclc0  49827  itscnhlinecirc02plem2  49839  itscnhlinecirc02plem3  49840  uptrlem1  50262  uptr2  50273  setc1onsubc  50654