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  7205  poseq  8098  oeeui  8527  oaabs2  8574  naddssim  8610  omxpenlem  9002  findcard3  9187  wemappo  9460  acndom2  9967  infpwfien  9975  sornom  10190  isf32lem2  10267  isf32lem4  10269  fin1a2lem11  10323  pwfseq  10577  gchina  10612  inttsk  10687  inar1  10688  prlem936  10960  mulcmpblnr  10984  00id  11309  mul02lem1  11310  addrid  11314  cnegex  11315  negeu  11371  add20  11650  ltmul12a  11998  lediv12a  12036  cru  12138  qextltlem  13122  xmullem  13184  xlemul1a  13208  ixxss12  13286  ioodisj  13403  elfz0fzfz0  13554  fsuppmapnn0fz  13921  seqf1o  13968  mulexpz  14027  leexp1a  14100  seqcoll  14389  swrdswrdlem  14628  pfxccatin12lem3  14656  abs3lem  15264  cau3lem  15280  climcau  15596  sumeq2ii  15618  climcndslem1  15774  climcndslem2  15775  geomulcvg  15801  mertenslem1  15809  mertenslem2  15810  mertens  15811  prodeq2ii  15836  prodmolem2  15860  bitsfzo  16364  sadadd2lem2  16379  dvdsmulgcd  16485  qredeu  16587  pc2dvds  16809  pcz  16811  ramcl  16959  firest  17354  mreexexlemd  17568  isacs2  17577  iscatd2  17605  ipodrsima  18465  mrelatlub  18486  mgmhmeql  18608  sgrppropd  18623  mndpropd  18651  mhmeql  18718  mhmid  18960  mhmmnd  18961  issubg4  19042  cycsubm  19099  cycsubmcom  19101  gasubg  19199  symgextf  19314  pmtr3ncom  19372  gexdvds  19481  oddvdssubg  19752  imasabl  19773  cyggeninv  19780  cyggenod  19781  submomnd  20029  issrg  20091  dvdsrmul1  20272  unitgrp  20286  cntzsubrng  20470  cntzsubr  20509  islmhm2  20960  lmhmeql  20977  lbspropd  21021  lssacsex  21069  rngqiprngimfo  21226  psgndiflemA  21526  isphl  21553  ocvocv  21596  lindfmm  21752  issubassa2  21817  mplbas2  21965  scmatmats  22414  smatvscl  22427  mdetdiag  22502  m2cpmfo  22659  pmatcollpw3fi1lem1  22689  pm2mpf1  22702  pm2mpghm  22719  fvmptnn04if  22752  chfacfscmulfsupp  22762  chfacfpmmulfsupp  22766  neissex  23030  neiptoptop  23034  neiptopnei  23035  restbas  23061  tgrest  23062  restopnb  23078  cnpco  23170  isreg2  23280  iunconn  23331  1stcrest  23356  2ndcctbss  23358  2ndcomap  23361  2ndcsep  23362  dislly  23400  kgencn2  23460  ptbasfi  23484  txhaus  23550  txkgen  23555  txconn  23592  qtopcn  23617  regr1lem2  23643  kqnrmlem1  23646  kqnrmlem2  23647  trfbas2  23746  trfil2  23790  flimcf  23885  hauspwpwf1  23890  fclscf  23928  flimfnfcls  23931  ustexsym  24119  ustuqtop4  24148  utop3cls  24155  utopreg  24156  ucnima  24184  ucncn  24188  metequiv2  24414  prdsxmslem2  24433  metcnpi3  24450  metustto  24457  metustid  24458  metustexhalf  24460  ngptgp  24540  xrsblre  24716  icccmp  24730  reconnlem1  24731  reconn  24733  opnreen  24736  metdsf  24753  metdscn  24761  mpomulcn  24774  fsumcn  24777  elcncf2  24799  cncfmet  24818  pcoass  24940  lmcau  25229  rrxdstprj1  25325  pmltpc  25367  ivthlem2  25369  ivthlem3  25370  ovollb2  25406  volsup  25473  ioombl1  25479  ioorf  25490  dyadss  25511  dyaddisjlem  25512  dyadmax  25515  volcn  25523  cncombf  25575  mbflimsup  25583  itg2const2  25658  iblss2  25723  cpnord  25853  dvmptfsum  25895  fta1g  26091  plydivex  26221  fta1  26232  aannenlem1  26252  ulmdvlem3  26327  advlogexp  26580  cxpmul2z  26616  atantayl2  26864  jensen  26915  isppw2  27041  lgsqr  27278  lgsqrmodndvds  27280  lgsdchrval  27281  lgsquad3  27314  2sqb  27359  dchrisumlem3  27418  pntrsumbnd2  27494  noinfbnd1lem5  27655  noetasuplem4  27664  noetainflem4  27668  noetalem1  27669  conway  27728  eqscut3  27753  madebdayim  27820  madebdaylemlrcut  27831  negsprop  27964  mulscom  28065  absmuls  28169  bdayon  28196  remulscl  28389  tgjustf  28436  axsegcon  28890  axeuclidlem  28925  axcontlem9  28935  eengtrkg  28949  cusgrsize2inds  29417  pthdepisspth  29698  usgr2wlkneq  29719  crctcshwlkn0  29784  wpthswwlks2on  29924  clwwlkccatlem  29951  wwlksext2clwwlk  30019  umgr3v3e3cycl  30146  vdgn1frgrv2  30258  frgrwopreglem5  30283  frgrwopreg  30285  frgrhash2wsp  30294  numclwwlk1lem2fo  30320  vacn  30656  smcnlem  30659  0lno  30752  chocunii  31263  occl  31266  5oalem1  31616  3oalem2  31625  unoplin  31882  hmoplin  31904  lnconi  31995  kbass5  32082  mdslmd1lem1  32287  mdslmd1lem2  32288  mdsymlem2  32366  cdj1i  32395  opreu2reuALT  32439  unidifsnne  32498  disjabrex  32544  disjabrexf  32545  acunirnmpt  32616  fgreu  32629  suppovss  32637  xrge0infss  32716  xrofsup  32723  fsumiunle  32787  sgnmul  32793  sgnsub  32795  mgcf1o  32958  xrge0addgt0  32984  fzto1st1  33057  cyc3genpm  33107  cycpmgcl  33108  submarchi  33141  archiabllem1  33148  archiabllem2a  33149  isarchiofld  33154  rlocval  33212  imaslmod  33303  lindfpropd  33332  unitprodclb  33339  elrspunidl  33378  dfufd2lem  33499  lvecdim0  33581  constrmon  33713  constrextdg2  33718  locfinreflem  33809  zarcmplem  33850  rge0scvg  33918  lmxrge0  33921  lmdvg  33922  qqhval2  33951  esumrnmpt2  34037  esumfsup  34039  esumpcvgval  34047  esumcvg  34055  esumgect  34059  esumiun  34063  sigaclfu2  34090  sigainb  34105  insiga  34106  fiunelros  34143  measinblem  34189  measinb  34190  measdivcst  34193  measdivcstALTV  34194  omssubadd  34270  oddpwdc  34324  dstrvprob  34442  signsply0  34521  signstfvneq0  34542  bnj1408  35005  ptpconn  35208  sconnpi1  35214  resconn  35221  cvmliftmolem2  35257  cvmlift2lem12  35289  satfsschain  35339  satffunlem2lem1  35379  ifscgr  36020  cgrxfr  36031  outsideofeu  36107  linethru  36129  neibastop1  36335  dnicn  36468  irrdifflemf  37301  irrdiff  37302  fin2so  37589  matunitlindflem1  37598  matunitlindflem2  37599  poimirlem28  37630  poimirlem31  37633  mblfinlem2  37640  mblfinlem3  37641  itg2addnclem  37653  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  ssbnd  37770  totbndbnd  37771  prtlem10  38846  lssats  38993  lkrlss  39076  lshpset2N  39100  2dim  39452  islvol5  39561  paddasslem11  39812  pexmidlem8N  39959  ltrnid  40117  idltrn  40132  trlator0  40153  trlnidatb  40159  cdlemf2  40544  cdlemg2cex  40573  tendodi1  40766  tendodi2  40767  diblss  41152  dihopelvalcpre  41230  dih1dimatlem  41311  dihglblem6  41322  primrootscoprmpow  42075  posbezout  42076  aks6d1c4  42100  sticksstones22  42144  aks6d1c6isolem1  42150  aks6d1c6isolem2  42151  aks6d1c6lem5  42153  grpods  42170  unitscyglem3  42173  unitscyglem4  42174  remul01  42383  sn-subeu  42403  sn-0tie0  42427  prjspertr  42581  prjspersym  42583  0prjspnrel  42603  mzpsubst  42724  mzpcompact2lem  42727  eldioph2  42738  eldioph2b  42739  diophren  42789  pell14qrexpcl  42843  elpell1qr2  42848  monotoddzzfi  42918  acongtr  42954  acongrep  42956  jm2.19lem4  42968  jm2.26a  42976  jm2.26lem3  42977  jm2.26  42978  isnumbasgrplem2  43080  mendassa  43166  omord2lim  43276  cantnftermord  43296  tfsconcatfv1  43315  tfsconcatfv2  43316  naddcnffo  43340  naddcnfcom  43342  naddcnfid1  43343  naddgeoa  43370  clsk3nimkb  44016  prmunb2  44287  4an4132  44476  fiiuncl  45046  ssinc  45068  ssdec  45069  supxrgelem  45320  infxr  45350  cvgcaule  45474  mullimc  45601  mullimcf  45608  neglimc  45632  climleltrp  45661  climisp  45731  limsupresxr  45751  liminfresxr  45752  liminflimsupclim  45792  xlimliminflimsup  45847  icccncfext  45872  cncfiooicclem1  45878  fprodcncf  45885  dvnprodlem3  45933  iblcncfioo  45963  itgspltprt  45964  stoweidlem7  45992  stoweidlem28  46013  stoweidlem34  46019  stoweidlem48  46033  stoweidlem52  46037  wallispilem3  46052  fourierdlem12  46104  fourierdlem38  46130  fourierdlem39  46131  fourierdlem42  46134  fourierdlem46  46137  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem65  46156  fourierdlem73  46164  fourierdlem76  46167  fourierdlem87  46178  fourierdlem103  46194  fourierdlem104  46195  sge0f1o  46367  sge0le  46392  sge0reuz  46432  ismeannd  46452  isomenndlem  46515  hoicvr  46533  hoidmvle  46585  smflimlem2  46757  smflimmpt  46795  fsupdm  46827  finfdm  46831  imasetpreimafvbijlemf1  47392  nnsum4primeseven  47788  nnsum4primesevenALTV  47789  bgoldbtbndlem2  47794  bgoldbtbndlem3  47795  bgoldbtbnd  47797  isubgr3stgrlem6  47959  rrxlinec  48725  iccdisj  48886  upfval  49165  fullthinc  49439