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  7204  poseq  8094  oeeui  8523  oaabs2  8570  naddssim  8606  omxpenlem  8998  findcard3  9174  wemappo  9442  acndom2  9952  infpwfien  9960  sornom  10175  isf32lem2  10252  isf32lem4  10254  fin1a2lem11  10308  pwfseq  10562  gchina  10597  inttsk  10672  inar1  10673  prlem936  10945  mulcmpblnr  10969  00id  11295  mul02lem1  11296  addrid  11300  cnegex  11301  negeu  11357  add20  11636  ltmul12a  11984  lediv12a  12022  cru  12124  qextltlem  13103  xmullem  13165  xlemul1a  13189  ixxss12  13267  ioodisj  13384  elfz0fzfz0  13535  fsuppmapnn0fz  13905  seqf1o  13952  mulexpz  14011  leexp1a  14084  seqcoll  14373  swrdswrdlem  14613  pfxccatin12lem3  14641  abs3lem  15248  cau3lem  15264  climcau  15580  sumeq2ii  15602  climcndslem1  15758  climcndslem2  15759  geomulcvg  15785  mertenslem1  15793  mertenslem2  15794  mertens  15795  prodeq2ii  15820  prodmolem2  15844  bitsfzo  16348  sadadd2lem2  16363  dvdsmulgcd  16469  qredeu  16571  pc2dvds  16793  pcz  16795  ramcl  16943  firest  17338  mreexexlemd  17552  isacs2  17561  iscatd2  17589  ipodrsima  18449  mrelatlub  18470  mgmhmeql  18626  sgrppropd  18641  mndpropd  18669  mhmeql  18736  mhmid  18978  mhmmnd  18979  issubg4  19060  cycsubm  19116  cycsubmcom  19118  gasubg  19216  symgextf  19331  pmtr3ncom  19389  gexdvds  19498  oddvdssubg  19769  imasabl  19790  cyggeninv  19797  cyggenod  19798  submomnd  20046  issrg  20108  dvdsrmul1  20289  unitgrp  20303  cntzsubrng  20484  cntzsubr  20523  islmhm2  20974  lmhmeql  20991  lbspropd  21035  lssacsex  21083  rngqiprngimfo  21240  psgndiflemA  21540  isphl  21567  ocvocv  21610  lindfmm  21766  issubassa2  21831  mplbas2  21978  scmatmats  22427  smatvscl  22440  mdetdiag  22515  m2cpmfo  22672  pmatcollpw3fi1lem1  22702  pm2mpf1  22715  pm2mpghm  22732  fvmptnn04if  22765  chfacfscmulfsupp  22775  chfacfpmmulfsupp  22779  neissex  23043  neiptoptop  23047  neiptopnei  23048  restbas  23074  tgrest  23075  restopnb  23091  cnpco  23183  isreg2  23293  iunconn  23344  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  2ndcsep  23375  dislly  23413  kgencn2  23473  ptbasfi  23497  txhaus  23563  txkgen  23568  txconn  23605  qtopcn  23630  regr1lem2  23656  kqnrmlem1  23659  kqnrmlem2  23660  trfbas2  23759  trfil2  23803  flimcf  23898  hauspwpwf1  23903  fclscf  23941  flimfnfcls  23944  ustexsym  24132  ustuqtop4  24160  utop3cls  24167  utopreg  24168  ucnima  24196  ucncn  24200  metequiv2  24426  prdsxmslem2  24445  metcnpi3  24462  metustto  24469  metustid  24470  metustexhalf  24472  ngptgp  24552  xrsblre  24728  icccmp  24742  reconnlem1  24743  reconn  24745  opnreen  24748  metdsf  24765  metdscn  24773  mpomulcn  24786  fsumcn  24789  elcncf2  24811  cncfmet  24830  pcoass  24952  lmcau  25241  rrxdstprj1  25337  pmltpc  25379  ivthlem2  25381  ivthlem3  25382  ovollb2  25418  volsup  25485  ioombl1  25491  ioorf  25502  dyadss  25523  dyaddisjlem  25524  dyadmax  25527  volcn  25535  cncombf  25587  mbflimsup  25595  itg2const2  25670  iblss2  25735  cpnord  25865  dvmptfsum  25907  fta1g  26103  plydivex  26233  fta1  26244  aannenlem1  26264  ulmdvlem3  26339  advlogexp  26592  cxpmul2z  26628  atantayl2  26876  jensen  26927  isppw2  27053  lgsqr  27290  lgsqrmodndvds  27292  lgsdchrval  27293  lgsquad3  27326  2sqb  27371  dchrisumlem3  27430  pntrsumbnd2  27506  noinfbnd1lem5  27667  noetasuplem4  27676  noetainflem4  27680  noetalem1  27681  conway  27741  eqscut3  27766  madebdayim  27834  madebdaylemlrcut  27845  negsprop  27978  mulscom  28079  absmuls  28183  bdayon  28210  remulscl  28405  tgjustf  28452  axsegcon  28907  axeuclidlem  28942  axcontlem9  28952  eengtrkg  28966  cusgrsize2inds  29434  pthdepisspth  29715  usgr2wlkneq  29736  crctcshwlkn0  29801  wpthswwlks2on  29944  clwwlkccatlem  29971  wwlksext2clwwlk  30039  umgr3v3e3cycl  30166  vdgn1frgrv2  30278  frgrwopreglem5  30303  frgrwopreg  30305  frgrhash2wsp  30314  numclwwlk1lem2fo  30340  vacn  30676  smcnlem  30679  0lno  30772  chocunii  31283  occl  31286  5oalem1  31636  3oalem2  31645  unoplin  31902  hmoplin  31924  lnconi  32015  kbass5  32102  mdslmd1lem1  32307  mdslmd1lem2  32308  mdsymlem2  32386  cdj1i  32415  opreu2reuALT  32458  unidifsnne  32518  disjabrex  32564  disjabrexf  32565  acunirnmpt  32643  fgreu  32656  suppovss  32666  xrge0infss  32747  xrofsup  32754  fsumiunle  32817  sgnmul  32823  sgnsub  32825  mgcf1o  32991  xrge0addgt0  33005  fzto1st1  33078  cyc3genpm  33128  cycpmgcl  33129  submarchi  33162  archiabllem1  33169  archiabllem2a  33170  isarchiofld  33175  rlocval  33233  imaslmod  33325  lindfpropd  33354  unitprodclb  33361  elrspunidl  33400  dfufd2lem  33521  mplmulmvr  33590  lvecdim0  33640  constrmon  33778  constrextdg2  33783  locfinreflem  33874  zarcmplem  33915  rge0scvg  33983  lmxrge0  33986  lmdvg  33987  qqhval2  34016  esumrnmpt2  34102  esumfsup  34104  esumpcvgval  34112  esumcvg  34120  esumgect  34124  esumiun  34128  sigaclfu2  34155  sigainb  34170  insiga  34171  fiunelros  34208  measinblem  34254  measinb  34255  measdivcst  34258  measdivcstALTV  34259  omssubadd  34334  oddpwdc  34388  dstrvprob  34506  signsply0  34585  signstfvneq0  34606  bnj1408  35069  ptpconn  35298  sconnpi1  35304  resconn  35311  cvmliftmolem2  35347  cvmlift2lem12  35379  satfsschain  35429  satffunlem2lem1  35469  ifscgr  36109  cgrxfr  36120  outsideofeu  36196  linethru  36218  neibastop1  36424  dnicn  36557  irrdifflemf  37390  irrdiff  37391  fin2so  37668  matunitlindflem1  37677  matunitlindflem2  37678  poimirlem28  37709  poimirlem31  37712  mblfinlem2  37719  mblfinlem3  37720  itg2addnclem  37732  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  ssbnd  37849  totbndbnd  37850  prtlem10  38985  lssats  39132  lkrlss  39215  lshpset2N  39239  2dim  39590  islvol5  39699  paddasslem11  39950  pexmidlem8N  40097  ltrnid  40255  idltrn  40270  trlator0  40291  trlnidatb  40297  cdlemf2  40682  cdlemg2cex  40711  tendodi1  40904  tendodi2  40905  diblss  41290  dihopelvalcpre  41368  dih1dimatlem  41449  dihglblem6  41460  primrootscoprmpow  42213  posbezout  42214  aks6d1c4  42238  sticksstones22  42282  aks6d1c6isolem1  42288  aks6d1c6isolem2  42289  aks6d1c6lem5  42291  grpods  42308  unitscyglem3  42311  unitscyglem4  42312  remul01  42526  sn-subeu  42546  sn-0tie0  42570  prjspertr  42724  prjspersym  42726  0prjspnrel  42746  mzpsubst  42866  mzpcompact2lem  42869  eldioph2  42880  eldioph2b  42881  diophren  42931  pell14qrexpcl  42985  elpell1qr2  42990  monotoddzzfi  43060  acongtr  43096  acongrep  43098  jm2.19lem4  43110  jm2.26a  43118  jm2.26lem3  43119  jm2.26  43120  isnumbasgrplem2  43222  mendassa  43308  omord2lim  43418  cantnftermord  43438  tfsconcatfv1  43457  tfsconcatfv2  43458  naddcnffo  43482  naddcnfcom  43484  naddcnfid1  43485  naddgeoa  43512  clsk3nimkb  44158  prmunb2  44429  4an4132  44617  fiiuncl  45187  ssinc  45209  ssdec  45210  supxrgelem  45461  infxr  45490  cvgcaule  45614  mullimc  45741  mullimcf  45748  neglimc  45770  climleltrp  45799  climisp  45869  limsupresxr  45889  liminfresxr  45890  liminflimsupclim  45930  xlimliminflimsup  45985  icccncfext  46010  cncfiooicclem1  46016  fprodcncf  46023  dvnprodlem3  46071  iblcncfioo  46101  itgspltprt  46102  stoweidlem7  46130  stoweidlem28  46151  stoweidlem34  46157  stoweidlem48  46171  stoweidlem52  46175  wallispilem3  46190  fourierdlem12  46242  fourierdlem38  46268  fourierdlem39  46269  fourierdlem42  46272  fourierdlem46  46275  fourierdlem48  46277  fourierdlem49  46278  fourierdlem50  46279  fourierdlem51  46280  fourierdlem65  46294  fourierdlem73  46302  fourierdlem76  46305  fourierdlem87  46316  fourierdlem103  46332  fourierdlem104  46333  sge0f1o  46505  sge0le  46530  sge0reuz  46570  ismeannd  46590  isomenndlem  46653  hoicvr  46671  hoidmvle  46723  smflimlem2  46895  smflimmpt  46933  fsupdm  46965  finfdm  46969  imasetpreimafvbijlemf1  47529  nnsum4primeseven  47925  nnsum4primesevenALTV  47926  bgoldbtbndlem2  47931  bgoldbtbndlem3  47932  bgoldbtbnd  47934  isubgr3stgrlem6  48096  rrxlinec  48862  iccdisj  49023  upfval  49302  fullthinc  49576