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 397

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 398

This theorem is referenced by:  f1imass  7169  oeeui  8464  oaabs2  8510  omxpenlem  8898  wemappo  9352  acndom2  9856  infpwfien  9864  sornom  10079  isf32lem2  10156  isf32lem4  10158  fin1a2lem11  10212  pwfseq  10466  gchina  10501  inttsk  10576  inar1  10577  prlem936  10849  mulcmpblnr  10873  00id  11196  mul02lem1  11197  addid1  11201  cnegex  11202  negeu  11257  add20  11533  ltmul12a  11877  lediv12a  11914  cru  12011  qextltlem  12982  xmullem  13044  xlemul1a  13068  ixxss12  13145  ioodisj  13260  elfz0fzfz0  13407  fsuppmapnn0fz  13762  seqf1o  13810  mulexpz  13869  leexp1a  13939  seqcoll  14223  swrdswrdlem  14462  pfxccatin12lem3  14490  abs3lem  15095  cau3lem  15111  climcau  15427  sumeq2ii  15450  climcndslem1  15606  climcndslem2  15607  geomulcvg  15633  mertenslem1  15641  mertenslem2  15642  mertens  15643  prodeq2ii  15668  prodmolem2  15690  bitsfzo  16187  sadadd2lem2  16202  dvdsmulgcd  16310  qredeu  16408  pc2dvds  16625  pcz  16627  ramcl  16775  firest  17188  mreexexlemd  17398  isacs2  17407  iscatd2  17435  ipodrsima  18304  mrelatlub  18325  mndpropd  18455  mhmeql  18509  mhmid  18741  mhmmnd  18742  issubg4  18819  cycsubm  18866  cycsubmcom  18868  gasubg  18953  symgextf  19070  pmtr3ncom  19128  gexdvds  19234  oddvdssubg  19501  cyggeninv  19528  cyggenod  19529  issrg  19788  dvdsrmul1  19940  unitgrp  19954  cntzsubr  20102  islmhm2  20345  lmhmeql  20362  lbspropd  20406  lssacsex  20451  psgndiflemA  20851  isphl  20878  ocvocv  20921  lindfmm  21079  issubassa2  21141  mplbas2  21288  scmatmats  21705  smatvscl  21718  mdetdiag  21793  m2cpmfo  21950  pmatcollpw3fi1lem1  21980  pm2mpf1  21993  pm2mpghm  22010  fvmptnn04if  22043  chfacfscmulfsupp  22053  chfacfpmmulfsupp  22057  neissex  22323  neiptoptop  22327  neiptopnei  22328  restbas  22354  tgrest  22355  restopnb  22371  cnpco  22463  isreg2  22573  iunconn  22624  1stcrest  22649  2ndcctbss  22651  2ndcomap  22654  2ndcsep  22655  dislly  22693  kgencn2  22753  ptbasfi  22777  txhaus  22843  txkgen  22848  txconn  22885  qtopcn  22910  regr1lem2  22936  kqnrmlem1  22939  kqnrmlem2  22940  trfbas2  23039  trfil2  23083  flimcf  23178  hauspwpwf1  23183  fclscf  23221  flimfnfcls  23224  ustexsym  23412  ustuqtop4  23441  utop3cls  23448  utopreg  23449  ucnima  23478  ucncn  23482  metequiv2  23711  prdsxmslem2  23730  metcnpi3  23747  metustto  23754  metustid  23755  metustexhalf  23757  ngptgp  23837  xrsblre  24019  icccmp  24033  reconnlem1  24034  reconn  24036  opnreen  24039  metdsf  24056  metdscn  24064  fsumcn  24078  elcncf2  24098  cncfmet  24117  pcoass  24232  lmcau  24522  rrxdstprj1  24618  pmltpc  24659  ivthlem2  24661  ivthlem3  24662  ovollb2  24698  volsup  24765  ioombl1  24771  ioorf  24782  dyadss  24803  dyaddisjlem  24804  dyadmax  24807  volcn  24815  cncombf  24867  mbflimsup  24875  itg2const2  24951  iblss2  25015  cpnord  25144  dvmptfsum  25184  fta1g  25377  plydivex  25502  fta1  25513  aannenlem1  25533  ulmdvlem3  25606  advlogexp  25855  cxpmul2z  25891  atantayl2  26133  jensen  26183  isppw2  26309  lgsqr  26544  lgsqrmodndvds  26546  lgsdchrval  26547  lgsquad3  26580  2sqb  26625  dchrisumlem3  26684  pntrsumbnd2  26760  tgjustf  26879  axsegcon  27340  axeuclidlem  27375  axcontlem9  27385  eengtrkg  27399  cusgrsize2inds  27865  pthdepisspth  28148  usgr2wlkneq  28169  crctcshwlkn0  28231  wpthswwlks2on  28371  clwwlkccatlem  28398  wwlksext2clwwlk  28466  umgr3v3e3cycl  28593  vdgn1frgrv2  28705  frgrwopreglem5  28730  frgrwopreg  28732  frgrhash2wsp  28741  numclwwlk1lem2fo  28767  vacn  29101  smcnlem  29104  0lno  29197  chocunii  29708  occl  29711  5oalem1  30061  3oalem2  30070  unoplin  30327  hmoplin  30349  lnconi  30440  kbass5  30527  mdslmd1lem1  30732  mdslmd1lem2  30733  mdsymlem2  30811  cdj1i  30840  opreu2reuALT  30870  unidifsnne  30929  disjabrex  30966  disjabrexf  30967  acunirnmpt  31041  fgreu  31054  suppovss  31062  xrge0infss  31128  xrofsup  31135  fsumiunle  31188  mgcf1o  31326  xrge0addgt0  31345  submomnd  31381  fzto1st1  31414  cyc3genpm  31464  cycpmgcl  31465  submarchi  31485  archiabllem1  31492  archiabllem2a  31493  isarchiofld  31561  imaslmod  31598  lindfpropd  31621  elrspunidl  31651  lvecdim0  31735  locfinreflem  31835  zarcmplem  31876  rge0scvg  31944  lmxrge0  31947  lmdvg  31948  qqhval2  31977  esumrnmpt2  32081  esumfsup  32083  esumpcvgval  32091  esumcvg  32099  esumgect  32103  esumiun  32107  sigaclfu2  32134  sigainb  32149  insiga  32150  fiunelros  32187  measinblem  32233  measinb  32234  measdivcst  32237  measdivcstALTV  32238  omssubadd  32312  oddpwdc  32366  dstrvprob  32483  sgnmul  32554  sgnsub  32556  signsply0  32575  signstfvneq0  32596  bnj1408  33061  ptpconn  33240  sconnpi1  33246  resconn  33253  cvmliftmolem2  33289  cvmlift2lem12  33321  satfsschain  33371  satffunlem2lem1  33411  poseq  33847  naddssim  33882  noinfbnd1lem5  33975  noetasuplem4  33984  noetainflem4  33988  noetalem1  33989  conway  34038  madebdayim  34115  madebdaylemlrcut  34124  ifscgr  34391  cgrxfr  34402  outsideofeu  34478  linethru  34500  neibastop1  34593  dnicn  34717  irrdifflemf  35540  irrdiff  35541  fin2so  35808  matunitlindflem1  35817  matunitlindflem2  35818  poimirlem28  35849  poimirlem31  35852  mblfinlem2  35859  mblfinlem3  35860  itg2addnclem  35872  ftc1anclem7  35900  ftc1anclem8  35901  ftc1anc  35902  ssbnd  35990  totbndbnd  35991  prtlem10  36921  lssats  37068  lkrlss  37151  lshpset2N  37175  2dim  37526  islvol5  37635  paddasslem11  37886  pexmidlem8N  38033  ltrnid  38191  idltrn  38206  trlator0  38227  trlnidatb  38233  cdlemf2  38618  cdlemg2cex  38647  tendodi1  38840  tendodi2  38841  diblss  39226  dihopelvalcpre  39304  dih1dimatlem  39385  dihglblem6  39396  sticksstones22  40166  remul01  40427  sn-subeu  40445  sn-0tie0  40458  itrere  40473  retire  40474  prjspertr  40481  prjspersym  40483  0prjspnrel  40501  mzpsubst  40607  mzpcompact2lem  40610  eldioph2  40621  eldioph2b  40622  diophren  40672  pell14qrexpcl  40726  elpell1qr2  40731  monotoddzzfi  40802  acongtr  40838  acongrep  40840  jm2.19lem4  40852  jm2.26a  40860  jm2.26lem3  40861  jm2.26  40862  isnumbasgrplem2  40967  mendassa  41057  clsk3nimkb  41688  prmunb2  41967  4an4132  42157  fiiuncl  42651  ssinc  42675  ssdec  42676  supxrgelem  42924  infxr  42954  mullimc  43206  mullimcf  43213  neglimc  43237  climleltrp  43266  climisp  43336  limsupresxr  43356  liminfresxr  43357  liminflimsupclim  43397  xlimliminflimsup  43452  icccncfext  43477  cncfiooicclem1  43483  fprodcncf  43490  dvnprodlem3  43538  iblcncfioo  43568  itgspltprt  43569  stoweidlem7  43597  stoweidlem28  43618  stoweidlem34  43624  stoweidlem48  43638  stoweidlem52  43642  wallispilem3  43657  fourierdlem12  43709  fourierdlem38  43735  fourierdlem39  43736  fourierdlem42  43739  fourierdlem46  43742  fourierdlem48  43744  fourierdlem49  43745  fourierdlem50  43746  fourierdlem51  43747  fourierdlem65  43761  fourierdlem73  43769  fourierdlem76  43772  fourierdlem87  43783  fourierdlem103  43799  fourierdlem104  43800  sge0f1o  43970  sge0le  43995  sge0reuz  44035  ismeannd  44055  isomenndlem  44118  hoicvr  44136  hoidmvle  44188  smflimlem2  44360  smflimmpt  44397  imasetpreimafvbijlemf1  44914  nnsum4primeseven  45310  nnsum4primesevenALTV  45311  bgoldbtbndlem2  45316  bgoldbtbndlem3  45317  bgoldbtbnd  45319  isomuspgrlem2  45343  mgmhmeql  45415  rrxlinec  46140  iccdisj  46250  fullthinc  46385