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  7198  poseq  8088  oeeui  8517  oaabs2  8564  naddssim  8600  omxpenlem  8991  findcard3  9167  wemappo  9435  acndom2  9945  infpwfien  9953  sornom  10168  isf32lem2  10245  isf32lem4  10247  fin1a2lem11  10301  pwfseq  10555  gchina  10590  inttsk  10665  inar1  10666  prlem936  10938  mulcmpblnr  10962  00id  11288  mul02lem1  11289  addrid  11293  cnegex  11294  negeu  11350  add20  11629  ltmul12a  11977  lediv12a  12015  cru  12117  qextltlem  13101  xmullem  13163  xlemul1a  13187  ixxss12  13265  ioodisj  13382  elfz0fzfz0  13533  fsuppmapnn0fz  13903  seqf1o  13950  mulexpz  14009  leexp1a  14082  seqcoll  14371  swrdswrdlem  14611  pfxccatin12lem3  14639  abs3lem  15246  cau3lem  15262  climcau  15578  sumeq2ii  15600  climcndslem1  15756  climcndslem2  15757  geomulcvg  15783  mertenslem1  15791  mertenslem2  15792  mertens  15793  prodeq2ii  15818  prodmolem2  15842  bitsfzo  16346  sadadd2lem2  16361  dvdsmulgcd  16467  qredeu  16569  pc2dvds  16791  pcz  16793  ramcl  16941  firest  17336  mreexexlemd  17550  isacs2  17559  iscatd2  17587  ipodrsima  18447  mrelatlub  18468  mgmhmeql  18624  sgrppropd  18639  mndpropd  18667  mhmeql  18734  mhmid  18976  mhmmnd  18977  issubg4  19058  cycsubm  19114  cycsubmcom  19116  gasubg  19214  symgextf  19329  pmtr3ncom  19387  gexdvds  19496  oddvdssubg  19767  imasabl  19788  cyggeninv  19795  cyggenod  19796  submomnd  20044  issrg  20106  dvdsrmul1  20287  unitgrp  20301  cntzsubrng  20482  cntzsubr  20521  islmhm2  20972  lmhmeql  20989  lbspropd  21033  lssacsex  21081  rngqiprngimfo  21238  psgndiflemA  21538  isphl  21565  ocvocv  21608  lindfmm  21764  issubassa2  21829  mplbas2  21977  scmatmats  22426  smatvscl  22439  mdetdiag  22514  m2cpmfo  22671  pmatcollpw3fi1lem1  22701  pm2mpf1  22714  pm2mpghm  22731  fvmptnn04if  22764  chfacfscmulfsupp  22774  chfacfpmmulfsupp  22778  neissex  23042  neiptoptop  23046  neiptopnei  23047  restbas  23073  tgrest  23074  restopnb  23090  cnpco  23182  isreg2  23292  iunconn  23343  1stcrest  23368  2ndcctbss  23370  2ndcomap  23373  2ndcsep  23374  dislly  23412  kgencn2  23472  ptbasfi  23496  txhaus  23562  txkgen  23567  txconn  23604  qtopcn  23629  regr1lem2  23655  kqnrmlem1  23658  kqnrmlem2  23659  trfbas2  23758  trfil2  23802  flimcf  23897  hauspwpwf1  23902  fclscf  23940  flimfnfcls  23943  ustexsym  24131  ustuqtop4  24159  utop3cls  24166  utopreg  24167  ucnima  24195  ucncn  24199  metequiv2  24425  prdsxmslem2  24444  metcnpi3  24461  metustto  24468  metustid  24469  metustexhalf  24471  ngptgp  24551  xrsblre  24727  icccmp  24741  reconnlem1  24742  reconn  24744  opnreen  24747  metdsf  24764  metdscn  24772  mpomulcn  24785  fsumcn  24788  elcncf2  24810  cncfmet  24829  pcoass  24951  lmcau  25240  rrxdstprj1  25336  pmltpc  25378  ivthlem2  25380  ivthlem3  25381  ovollb2  25417  volsup  25484  ioombl1  25490  ioorf  25501  dyadss  25522  dyaddisjlem  25523  dyadmax  25526  volcn  25534  cncombf  25586  mbflimsup  25594  itg2const2  25669  iblss2  25734  cpnord  25864  dvmptfsum  25906  fta1g  26102  plydivex  26232  fta1  26243  aannenlem1  26263  ulmdvlem3  26338  advlogexp  26591  cxpmul2z  26627  atantayl2  26875  jensen  26926  isppw2  27052  lgsqr  27289  lgsqrmodndvds  27291  lgsdchrval  27292  lgsquad3  27325  2sqb  27370  dchrisumlem3  27429  pntrsumbnd2  27505  noinfbnd1lem5  27666  noetasuplem4  27675  noetainflem4  27679  noetalem1  27680  conway  27740  eqscut3  27765  madebdayim  27833  madebdaylemlrcut  27844  negsprop  27977  mulscom  28078  absmuls  28182  bdayon  28209  remulscl  28404  tgjustf  28451  axsegcon  28905  axeuclidlem  28940  axcontlem9  28950  eengtrkg  28964  cusgrsize2inds  29432  pthdepisspth  29713  usgr2wlkneq  29734  crctcshwlkn0  29799  wpthswwlks2on  29942  clwwlkccatlem  29969  wwlksext2clwwlk  30037  umgr3v3e3cycl  30164  vdgn1frgrv2  30276  frgrwopreglem5  30301  frgrwopreg  30303  frgrhash2wsp  30312  numclwwlk1lem2fo  30338  vacn  30674  smcnlem  30677  0lno  30770  chocunii  31281  occl  31284  5oalem1  31634  3oalem2  31643  unoplin  31900  hmoplin  31922  lnconi  32013  kbass5  32100  mdslmd1lem1  32305  mdslmd1lem2  32306  mdsymlem2  32384  cdj1i  32413  opreu2reuALT  32456  unidifsnne  32516  disjabrex  32562  disjabrexf  32563  acunirnmpt  32641  fgreu  32654  suppovss  32662  xrge0infss  32743  xrofsup  32750  fsumiunle  32812  sgnmul  32818  sgnsub  32820  mgcf1o  32984  xrge0addgt0  32998  fzto1st1  33071  cyc3genpm  33121  cycpmgcl  33122  submarchi  33155  archiabllem1  33162  archiabllem2a  33163  isarchiofld  33168  rlocval  33226  imaslmod  33318  lindfpropd  33347  unitprodclb  33354  elrspunidl  33393  dfufd2lem  33514  lvecdim0  33619  constrmon  33757  constrextdg2  33762  locfinreflem  33853  zarcmplem  33894  rge0scvg  33962  lmxrge0  33965  lmdvg  33966  qqhval2  33995  esumrnmpt2  34081  esumfsup  34083  esumpcvgval  34091  esumcvg  34099  esumgect  34103  esumiun  34107  sigaclfu2  34134  sigainb  34149  insiga  34150  fiunelros  34187  measinblem  34233  measinb  34234  measdivcst  34237  measdivcstALTV  34238  omssubadd  34313  oddpwdc  34367  dstrvprob  34485  signsply0  34564  signstfvneq0  34585  bnj1408  35048  ptpconn  35277  sconnpi1  35283  resconn  35290  cvmliftmolem2  35326  cvmlift2lem12  35358  satfsschain  35408  satffunlem2lem1  35448  ifscgr  36088  cgrxfr  36099  outsideofeu  36175  linethru  36197  neibastop1  36403  dnicn  36536  irrdifflemf  37369  irrdiff  37370  fin2so  37646  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem28  37687  poimirlem31  37690  mblfinlem2  37697  mblfinlem3  37698  itg2addnclem  37710  ftc1anclem7  37738  ftc1anclem8  37739  ftc1anc  37740  ssbnd  37827  totbndbnd  37828  prtlem10  38963  lssats  39110  lkrlss  39193  lshpset2N  39217  2dim  39568  islvol5  39677  paddasslem11  39928  pexmidlem8N  40075  ltrnid  40233  idltrn  40248  trlator0  40269  trlnidatb  40275  cdlemf2  40660  cdlemg2cex  40689  tendodi1  40882  tendodi2  40883  diblss  41268  dihopelvalcpre  41346  dih1dimatlem  41427  dihglblem6  41438  primrootscoprmpow  42191  posbezout  42192  aks6d1c4  42216  sticksstones22  42260  aks6d1c6isolem1  42266  aks6d1c6isolem2  42267  aks6d1c6lem5  42269  grpods  42286  unitscyglem3  42289  unitscyglem4  42290  remul01  42499  sn-subeu  42519  sn-0tie0  42543  prjspertr  42697  prjspersym  42699  0prjspnrel  42719  mzpsubst  42840  mzpcompact2lem  42843  eldioph2  42854  eldioph2b  42855  diophren  42905  pell14qrexpcl  42959  elpell1qr2  42964  monotoddzzfi  43034  acongtr  43070  acongrep  43072  jm2.19lem4  43084  jm2.26a  43092  jm2.26lem3  43093  jm2.26  43094  isnumbasgrplem2  43196  mendassa  43282  omord2lim  43392  cantnftermord  43412  tfsconcatfv1  43431  tfsconcatfv2  43432  naddcnffo  43456  naddcnfcom  43458  naddcnfid1  43459  naddgeoa  43486  clsk3nimkb  44132  prmunb2  44403  4an4132  44591  fiiuncl  45161  ssinc  45183  ssdec  45184  supxrgelem  45435  infxr  45464  cvgcaule  45588  mullimc  45715  mullimcf  45722  neglimc  45744  climleltrp  45773  climisp  45843  limsupresxr  45863  liminfresxr  45864  liminflimsupclim  45904  xlimliminflimsup  45959  icccncfext  45984  cncfiooicclem1  45990  fprodcncf  45997  dvnprodlem3  46045  iblcncfioo  46075  itgspltprt  46076  stoweidlem7  46104  stoweidlem28  46125  stoweidlem34  46131  stoweidlem48  46145  stoweidlem52  46149  wallispilem3  46164  fourierdlem12  46216  fourierdlem38  46242  fourierdlem39  46243  fourierdlem42  46246  fourierdlem46  46249  fourierdlem48  46251  fourierdlem49  46252  fourierdlem50  46253  fourierdlem51  46254  fourierdlem65  46268  fourierdlem73  46276  fourierdlem76  46279  fourierdlem87  46290  fourierdlem103  46306  fourierdlem104  46307  sge0f1o  46479  sge0le  46504  sge0reuz  46544  ismeannd  46564  isomenndlem  46627  hoicvr  46645  hoidmvle  46697  smflimlem2  46869  smflimmpt  46907  fsupdm  46939  finfdm  46943  imasetpreimafvbijlemf1  47503  nnsum4primeseven  47899  nnsum4primesevenALTV  47900  bgoldbtbndlem2  47905  bgoldbtbndlem3  47906  bgoldbtbnd  47908  isubgr3stgrlem6  48070  rrxlinec  48836  iccdisj  48997  upfval  49276  fullthinc  49550