Theorem simplll 774

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 730	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  f1imass  7256  poseq  8155  oeeui  8612  oaabs2  8659  naddssim  8695  omxpenlem  9085  findcard3  9288  wemappo  9561  acndom2  10066  infpwfien  10074  sornom  10289  isf32lem2  10366  isf32lem4  10368  fin1a2lem11  10422  pwfseq  10676  gchina  10711  inttsk  10786  inar1  10787  prlem936  11059  mulcmpblnr  11083  00id  11408  mul02lem1  11409  addrid  11413  cnegex  11414  negeu  11470  add20  11747  ltmul12a  12095  lediv12a  12133  cru  12230  qextltlem  13216  xmullem  13278  xlemul1a  13302  ixxss12  13380  ioodisj  13497  elfz0fzfz0  13648  fsuppmapnn0fz  14012  seqf1o  14059  mulexpz  14118  leexp1a  14191  seqcoll  14480  swrdswrdlem  14720  pfxccatin12lem3  14748  abs3lem  15355  cau3lem  15371  climcau  15685  sumeq2ii  15707  climcndslem1  15863  climcndslem2  15864  geomulcvg  15890  mertenslem1  15898  mertenslem2  15899  mertens  15900  prodeq2ii  15925  prodmolem2  15949  bitsfzo  16452  sadadd2lem2  16467  dvdsmulgcd  16573  qredeu  16675  pc2dvds  16897  pcz  16899  ramcl  17047  firest  17444  mreexexlemd  17654  isacs2  17663  iscatd2  17691  ipodrsima  18549  mrelatlub  18570  mgmhmeql  18692  sgrppropd  18707  mndpropd  18735  mhmeql  18802  mhmid  19044  mhmmnd  19045  issubg4  19126  cycsubm  19183  cycsubmcom  19185  gasubg  19283  symgextf  19396  pmtr3ncom  19454  gexdvds  19563  oddvdssubg  19834  imasabl  19855  cyggeninv  19862  cyggenod  19863  issrg  20146  dvdsrmul1  20327  unitgrp  20341  cntzsubrng  20525  cntzsubr  20564  islmhm2  20994  lmhmeql  21011  lbspropd  21055  lssacsex  21103  rngqiprngimfo  21260  psgndiflemA  21559  isphl  21586  ocvocv  21629  lindfmm  21785  issubassa2  21850  mplbas2  21998  scmatmats  22447  smatvscl  22460  mdetdiag  22535  m2cpmfo  22692  pmatcollpw3fi1lem1  22722  pm2mpf1  22735  pm2mpghm  22752  fvmptnn04if  22785  chfacfscmulfsupp  22795  chfacfpmmulfsupp  22799  neissex  23063  neiptoptop  23067  neiptopnei  23068  restbas  23094  tgrest  23095  restopnb  23111  cnpco  23203  isreg2  23313  iunconn  23364  1stcrest  23389  2ndcctbss  23391  2ndcomap  23394  2ndcsep  23395  dislly  23433  kgencn2  23493  ptbasfi  23517  txhaus  23583  txkgen  23588  txconn  23625  qtopcn  23650  regr1lem2  23676  kqnrmlem1  23679  kqnrmlem2  23680  trfbas2  23779  trfil2  23823  flimcf  23918  hauspwpwf1  23923  fclscf  23961  flimfnfcls  23964  ustexsym  24152  ustuqtop4  24181  utop3cls  24188  utopreg  24189  ucnima  24217  ucncn  24221  metequiv2  24447  prdsxmslem2  24466  metcnpi3  24483  metustto  24490  metustid  24491  metustexhalf  24493  ngptgp  24573  xrsblre  24749  icccmp  24763  reconnlem1  24764  reconn  24766  opnreen  24769  metdsf  24786  metdscn  24794  mpomulcn  24807  fsumcn  24810  elcncf2  24832  cncfmet  24851  pcoass  24973  lmcau  25263  rrxdstprj1  25359  pmltpc  25401  ivthlem2  25403  ivthlem3  25404  ovollb2  25440  volsup  25507  ioombl1  25513  ioorf  25524  dyadss  25545  dyaddisjlem  25546  dyadmax  25549  volcn  25557  cncombf  25609  mbflimsup  25617  itg2const2  25692  iblss2  25757  cpnord  25887  dvmptfsum  25929  fta1g  26125  plydivex  26255  fta1  26266  aannenlem1  26286  ulmdvlem3  26361  advlogexp  26614  cxpmul2z  26650  atantayl2  26898  jensen  26949  isppw2  27075  lgsqr  27312  lgsqrmodndvds  27314  lgsdchrval  27315  lgsquad3  27348  2sqb  27393  dchrisumlem3  27452  pntrsumbnd2  27528  noinfbnd1lem5  27689  noetasuplem4  27698  noetainflem4  27702  noetalem1  27703  conway  27761  madebdayim  27843  madebdaylemlrcut  27854  negsprop  27984  mulscom  28082  absmuls  28185  remulscl  28351  tgjustf  28398  axsegcon  28852  axeuclidlem  28887  axcontlem9  28897  eengtrkg  28911  cusgrsize2inds  29379  pthdepisspth  29663  usgr2wlkneq  29684  crctcshwlkn0  29749  wpthswwlks2on  29889  clwwlkccatlem  29916  wwlksext2clwwlk  29984  umgr3v3e3cycl  30111  vdgn1frgrv2  30223  frgrwopreglem5  30248  frgrwopreg  30250  frgrhash2wsp  30259  numclwwlk1lem2fo  30285  vacn  30621  smcnlem  30624  0lno  30717  chocunii  31228  occl  31231  5oalem1  31581  3oalem2  31590  unoplin  31847  hmoplin  31869  lnconi  31960  kbass5  32047  mdslmd1lem1  32252  mdslmd1lem2  32253  mdsymlem2  32331  cdj1i  32360  opreu2reuALT  32404  unidifsnne  32463  disjabrex  32509  disjabrexf  32510  acunirnmpt  32583  fgreu  32596  suppovss  32604  xrge0infss  32683  xrofsup  32690  fsumiunle  32754  sgnmul  32760  sgnsub  32762  mgcf1o  32929  xrge0addgt0  32958  submomnd  33024  fzto1st1  33059  cyc3genpm  33109  cycpmgcl  33110  submarchi  33130  archiabllem1  33137  archiabllem2a  33138  rlocval  33200  isarchiofld  33285  imaslmod  33314  lindfpropd  33343  unitprodclb  33350  elrspunidl  33389  dfufd2lem  33510  lvecdim0  33592  constrmon  33724  constrextdg2  33729  locfinreflem  33817  zarcmplem  33858  rge0scvg  33926  lmxrge0  33929  lmdvg  33930  qqhval2  33959  esumrnmpt2  34045  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  esumgect  34067  esumiun  34071  sigaclfu2  34098  sigainb  34113  insiga  34114  fiunelros  34151  measinblem  34197  measinb  34198  measdivcst  34201  measdivcstALTV  34202  omssubadd  34278  oddpwdc  34332  dstrvprob  34450  signsply0  34529  signstfvneq0  34550  bnj1408  35013  ptpconn  35201  sconnpi1  35207  resconn  35214  cvmliftmolem2  35250  cvmlift2lem12  35282  satfsschain  35332  satffunlem2lem1  35372  ifscgr  36008  cgrxfr  36019  outsideofeu  36095  linethru  36117  neibastop1  36323  dnicn  36456  irrdifflemf  37289  irrdiff  37290  fin2so  37577  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem28  37618  poimirlem31  37621  mblfinlem2  37628  mblfinlem3  37629  itg2addnclem  37641  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ssbnd  37758  totbndbnd  37759  prtlem10  38829  lssats  38976  lkrlss  39059  lshpset2N  39083  2dim  39435  islvol5  39544  paddasslem11  39795  pexmidlem8N  39942  ltrnid  40100  idltrn  40115  trlator0  40136  trlnidatb  40142  cdlemf2  40527  cdlemg2cex  40556  tendodi1  40749  tendodi2  40750  diblss  41135  dihopelvalcpre  41213  dih1dimatlem  41294  dihglblem6  41305  primrootscoprmpow  42058  posbezout  42059  aks6d1c4  42083  sticksstones22  42127  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6lem5  42136  grpods  42153  unitscyglem3  42156  unitscyglem4  42157  remul01  42397  sn-subeu  42416  sn-0tie0  42429  sn-itrere  42458  sn-retire  42459  prjspertr  42575  prjspersym  42577  0prjspnrel  42597  mzpsubst  42718  mzpcompact2lem  42721  eldioph2  42732  eldioph2b  42733  diophren  42783  pell14qrexpcl  42837  elpell1qr2  42842  monotoddzzfi  42913  acongtr  42949  acongrep  42951  jm2.19lem4  42963  jm2.26a  42971  jm2.26lem3  42972  jm2.26  42973  isnumbasgrplem2  43075  mendassa  43161  omord2lim  43271  cantnftermord  43291  tfsconcatfv1  43310  tfsconcatfv2  43311  naddcnffo  43335  naddcnfcom  43337  naddcnfid1  43338  naddgeoa  43365  clsk3nimkb  44011  prmunb2  44283  4an4132  44472  fiiuncl  45037  ssinc  45059  ssdec  45060  supxrgelem  45312  infxr  45342  cvgcaule  45466  mullimc  45593  mullimcf  45600  neglimc  45624  climleltrp  45653  climisp  45723  limsupresxr  45743  liminfresxr  45744  liminflimsupclim  45784  xlimliminflimsup  45839  icccncfext  45864  cncfiooicclem1  45870  fprodcncf  45877  dvnprodlem3  45925  iblcncfioo  45955  itgspltprt  45956  stoweidlem7  45984  stoweidlem28  46005  stoweidlem34  46011  stoweidlem48  46025  stoweidlem52  46029  wallispilem3  46044  fourierdlem12  46096  fourierdlem38  46122  fourierdlem39  46123  fourierdlem42  46126  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem65  46148  fourierdlem73  46156  fourierdlem76  46159  fourierdlem87  46170  fourierdlem103  46186  fourierdlem104  46187  sge0f1o  46359  sge0le  46384  sge0reuz  46424  ismeannd  46444  isomenndlem  46507  hoicvr  46525  hoidmvle  46577  smflimlem2  46749  smflimmpt  46787  fsupdm  46819  finfdm  46823  imasetpreimafvbijlemf1  47366  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  isubgr3stgrlem6  47931  rrxlinec  48664  iccdisj  48820  upfval  49059  fullthinc  49284