Theorem simplll 773

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.) (Proof shortened by Wolf Lammen, 6-Apr-2022.)

Assertion

Ref	Expression
simplll	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Proof of Theorem simplll

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	ad3antrrr 728	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396

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

This theorem is referenced by:  f1imass  7265  poseq  8146  oeeui  8604  oaabs2  8650  naddssim  8686  omxpenlem  9075  findcard3  9287  wemappo  9546  acndom2  10051  infpwfien  10059  sornom  10274  isf32lem2  10351  isf32lem4  10353  fin1a2lem11  10407  pwfseq  10661  gchina  10696  inttsk  10771  inar1  10772  prlem936  11044  mulcmpblnr  11068  00id  11393  mul02lem1  11394  addrid  11398  cnegex  11399  negeu  11454  add20  11730  ltmul12a  12074  lediv12a  12111  cru  12208  qextltlem  13185  xmullem  13247  xlemul1a  13271  ixxss12  13348  ioodisj  13463  elfz0fzfz0  13610  fsuppmapnn0fz  13965  seqf1o  14013  mulexpz  14072  leexp1a  14144  seqcoll  14429  swrdswrdlem  14658  pfxccatin12lem3  14686  abs3lem  15289  cau3lem  15305  climcau  15621  sumeq2ii  15643  climcndslem1  15799  climcndslem2  15800  geomulcvg  15826  mertenslem1  15834  mertenslem2  15835  mertens  15836  prodeq2ii  15861  prodmolem2  15883  bitsfzo  16380  sadadd2lem2  16395  dvdsmulgcd  16501  qredeu  16599  pc2dvds  16816  pcz  16818  ramcl  16966  firest  17382  mreexexlemd  17592  isacs2  17601  iscatd2  17629  ipodrsima  18498  mrelatlub  18519  mgmhmeql  18641  sgrppropd  18656  mndpropd  18684  mhmeql  18743  mhmid  18982  mhmmnd  18983  issubg4  19061  cycsubm  19117  cycsubmcom  19119  gasubg  19207  symgextf  19326  pmtr3ncom  19384  gexdvds  19493  oddvdssubg  19764  imasabl  19785  cyggeninv  19792  cyggenod  19793  issrg  20082  dvdsrmul1  20260  unitgrp  20274  cntzsubrng  20455  cntzsubr  20496  islmhm2  20793  lmhmeql  20810  lbspropd  20854  lssacsex  20902  rngqiprngimfo  21060  psgndiflemA  21373  isphl  21400  ocvocv  21443  lindfmm  21601  issubassa2  21665  mplbas2  21816  scmatmats  22233  smatvscl  22246  mdetdiag  22321  m2cpmfo  22478  pmatcollpw3fi1lem1  22508  pm2mpf1  22521  pm2mpghm  22538  fvmptnn04if  22571  chfacfscmulfsupp  22581  chfacfpmmulfsupp  22585  neissex  22851  neiptoptop  22855  neiptopnei  22856  restbas  22882  tgrest  22883  restopnb  22899  cnpco  22991  isreg2  23101  iunconn  23152  1stcrest  23177  2ndcctbss  23179  2ndcomap  23182  2ndcsep  23183  dislly  23221  kgencn2  23281  ptbasfi  23305  txhaus  23371  txkgen  23376  txconn  23413  qtopcn  23438  regr1lem2  23464  kqnrmlem1  23467  kqnrmlem2  23468  trfbas2  23567  trfil2  23611  flimcf  23706  hauspwpwf1  23711  fclscf  23749  flimfnfcls  23752  ustexsym  23940  ustuqtop4  23969  utop3cls  23976  utopreg  23977  ucnima  24006  ucncn  24010  metequiv2  24239  prdsxmslem2  24258  metcnpi3  24275  metustto  24282  metustid  24283  metustexhalf  24285  ngptgp  24365  xrsblre  24547  icccmp  24561  reconnlem1  24562  reconn  24564  opnreen  24567  metdsf  24584  metdscn  24592  mpomulcn  24605  fsumcn  24608  elcncf2  24630  cncfmet  24649  pcoass  24764  lmcau  25054  rrxdstprj1  25150  pmltpc  25191  ivthlem2  25193  ivthlem3  25194  ovollb2  25230  volsup  25297  ioombl1  25303  ioorf  25314  dyadss  25335  dyaddisjlem  25336  dyadmax  25339  volcn  25347  cncombf  25399  mbflimsup  25407  itg2const2  25483  iblss2  25547  cpnord  25676  dvmptfsum  25716  fta1g  25909  plydivex  26034  fta1  26045  aannenlem1  26065  ulmdvlem3  26138  advlogexp  26387  cxpmul2z  26423  atantayl2  26667  jensen  26717  isppw2  26843  lgsqr  27078  lgsqrmodndvds  27080  lgsdchrval  27081  lgsquad3  27114  2sqb  27159  dchrisumlem3  27218  pntrsumbnd2  27294  noinfbnd1lem5  27454  noetasuplem4  27463  noetainflem4  27467  noetalem1  27468  conway  27525  madebdayim  27607  madebdaylemlrcut  27618  negsprop  27736  mulscom  27822  tgjustf  27979  axsegcon  28440  axeuclidlem  28475  axcontlem9  28485  eengtrkg  28499  cusgrsize2inds  28965  pthdepisspth  29247  usgr2wlkneq  29268  crctcshwlkn0  29330  wpthswwlks2on  29470  clwwlkccatlem  29497  wwlksext2clwwlk  29565  umgr3v3e3cycl  29692  vdgn1frgrv2  29804  frgrwopreglem5  29829  frgrwopreg  29831  frgrhash2wsp  29840  numclwwlk1lem2fo  29866  vacn  30202  smcnlem  30205  0lno  30298  chocunii  30809  occl  30812  5oalem1  31162  3oalem2  31171  unoplin  31428  hmoplin  31450  lnconi  31541  kbass5  31628  mdslmd1lem1  31833  mdslmd1lem2  31834  mdsymlem2  31912  cdj1i  31941  opreu2reuALT  31972  unidifsnne  32028  disjabrex  32068  disjabrexf  32069  acunirnmpt  32139  fgreu  32152  suppovss  32161  xrge0infss  32228  xrofsup  32235  fsumiunle  32290  mgcf1o  32428  xrge0addgt0  32447  submomnd  32486  fzto1st1  32519  cyc3genpm  32569  cycpmgcl  32570  submarchi  32590  archiabllem1  32597  archiabllem2a  32598  isarchiofld  32693  imaslmod  32726  lindfpropd  32760  elrspunidl  32808  lvecdim0  32967  locfinreflem  33106  zarcmplem  33147  rge0scvg  33215  lmxrge0  33218  lmdvg  33219  qqhval2  33248  esumrnmpt2  33352  esumfsup  33354  esumpcvgval  33362  esumcvg  33370  esumgect  33374  esumiun  33378  sigaclfu2  33405  sigainb  33420  insiga  33421  fiunelros  33458  measinblem  33504  measinb  33505  measdivcst  33508  measdivcstALTV  33509  omssubadd  33585  oddpwdc  33639  dstrvprob  33756  sgnmul  33827  sgnsub  33829  signsply0  33848  signstfvneq0  33869  bnj1408  34333  ptpconn  34510  sconnpi1  34516  resconn  34523  cvmliftmolem2  34559  cvmlift2lem12  34591  satfsschain  34641  satffunlem2lem1  34681  ifscgr  35308  cgrxfr  35319  outsideofeu  35395  linethru  35417  neibastop1  35547  dnicn  35671  irrdifflemf  36509  irrdiff  36510  fin2so  36778  matunitlindflem1  36787  matunitlindflem2  36788  poimirlem28  36819  poimirlem31  36822  mblfinlem2  36829  mblfinlem3  36830  itg2addnclem  36842  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  ssbnd  36959  totbndbnd  36960  prtlem10  38038  lssats  38185  lkrlss  38268  lshpset2N  38292  2dim  38644  islvol5  38753  paddasslem11  39004  pexmidlem8N  39151  ltrnid  39309  idltrn  39324  trlator0  39345  trlnidatb  39351  cdlemf2  39736  cdlemg2cex  39765  tendodi1  39958  tendodi2  39959  diblss  40344  dihopelvalcpre  40422  dih1dimatlem  40503  dihglblem6  40514  sticksstones22  41290  remul01  41582  sn-subeu  41601  sn-0tie0  41614  itrere  41641  retire  41642  prjspertr  41649  prjspersym  41651  0prjspnrel  41671  mzpsubst  41788  mzpcompact2lem  41791  eldioph2  41802  eldioph2b  41803  diophren  41853  pell14qrexpcl  41907  elpell1qr2  41912  monotoddzzfi  41983  acongtr  42019  acongrep  42021  jm2.19lem4  42033  jm2.26a  42041  jm2.26lem3  42042  jm2.26  42043  isnumbasgrplem2  42148  mendassa  42238  omord2lim  42352  cantnftermord  42372  tfsconcatfv1  42391  tfsconcatfv2  42392  naddcnffo  42416  naddcnfcom  42418  naddcnfid1  42419  naddgeoa  42447  clsk3nimkb  43093  prmunb2  43372  4an4132  43562  fiiuncl  44054  ssinc  44078  ssdec  44079  supxrgelem  44346  infxr  44376  cvgcaule  44501  mullimc  44631  mullimcf  44638  neglimc  44662  climleltrp  44691  climisp  44761  limsupresxr  44781  liminfresxr  44782  liminflimsupclim  44822  xlimliminflimsup  44877  icccncfext  44902  cncfiooicclem1  44908  fprodcncf  44915  dvnprodlem3  44963  iblcncfioo  44993  itgspltprt  44994  stoweidlem7  45022  stoweidlem28  45043  stoweidlem34  45049  stoweidlem48  45063  stoweidlem52  45067  wallispilem3  45082  fourierdlem12  45134  fourierdlem38  45160  fourierdlem39  45161  fourierdlem42  45164  fourierdlem46  45167  fourierdlem48  45169  fourierdlem49  45170  fourierdlem50  45171  fourierdlem51  45172  fourierdlem65  45186  fourierdlem73  45194  fourierdlem76  45197  fourierdlem87  45208  fourierdlem103  45224  fourierdlem104  45225  sge0f1o  45397  sge0le  45422  sge0reuz  45462  ismeannd  45482  isomenndlem  45545  hoicvr  45563  hoidmvle  45615  smflimlem2  45787  smflimmpt  45825  fsupdm  45857  finfdm  45861  imasetpreimafvbijlemf1  46371  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  bgoldbtbndlem2  46773  bgoldbtbndlem3  46774  bgoldbtbnd  46776  isomuspgrlem2  46800  rrxlinec  47510  iccdisj  47619  fullthinc  47754