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  7239  poseq  8137  oeeui  8566  oaabs2  8613  naddssim  8649  omxpenlem  9042  findcard3  9229  wemappo  9502  acndom2  10007  infpwfien  10015  sornom  10230  isf32lem2  10307  isf32lem4  10309  fin1a2lem11  10363  pwfseq  10617  gchina  10652  inttsk  10727  inar1  10728  prlem936  11000  mulcmpblnr  11024  00id  11349  mul02lem1  11350  addrid  11354  cnegex  11355  negeu  11411  add20  11690  ltmul12a  12038  lediv12a  12076  cru  12178  qextltlem  13162  xmullem  13224  xlemul1a  13248  ixxss12  13326  ioodisj  13443  elfz0fzfz0  13594  fsuppmapnn0fz  13961  seqf1o  14008  mulexpz  14067  leexp1a  14140  seqcoll  14429  swrdswrdlem  14669  pfxccatin12lem3  14697  abs3lem  15305  cau3lem  15321  climcau  15637  sumeq2ii  15659  climcndslem1  15815  climcndslem2  15816  geomulcvg  15842  mertenslem1  15850  mertenslem2  15851  mertens  15852  prodeq2ii  15877  prodmolem2  15901  bitsfzo  16405  sadadd2lem2  16420  dvdsmulgcd  16526  qredeu  16628  pc2dvds  16850  pcz  16852  ramcl  17000  firest  17395  mreexexlemd  17605  isacs2  17614  iscatd2  17642  ipodrsima  18500  mrelatlub  18521  mgmhmeql  18643  sgrppropd  18658  mndpropd  18686  mhmeql  18753  mhmid  18995  mhmmnd  18996  issubg4  19077  cycsubm  19134  cycsubmcom  19136  gasubg  19234  symgextf  19347  pmtr3ncom  19405  gexdvds  19514  oddvdssubg  19785  imasabl  19806  cyggeninv  19813  cyggenod  19814  issrg  20097  dvdsrmul1  20278  unitgrp  20292  cntzsubrng  20476  cntzsubr  20515  islmhm2  20945  lmhmeql  20962  lbspropd  21006  lssacsex  21054  rngqiprngimfo  21211  psgndiflemA  21510  isphl  21537  ocvocv  21580  lindfmm  21736  issubassa2  21801  mplbas2  21949  scmatmats  22398  smatvscl  22411  mdetdiag  22486  m2cpmfo  22643  pmatcollpw3fi1lem1  22673  pm2mpf1  22686  pm2mpghm  22703  fvmptnn04if  22736  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  neissex  23014  neiptoptop  23018  neiptopnei  23019  restbas  23045  tgrest  23046  restopnb  23062  cnpco  23154  isreg2  23264  iunconn  23315  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  2ndcsep  23346  dislly  23384  kgencn2  23444  ptbasfi  23468  txhaus  23534  txkgen  23539  txconn  23576  qtopcn  23601  regr1lem2  23627  kqnrmlem1  23630  kqnrmlem2  23631  trfbas2  23730  trfil2  23774  flimcf  23869  hauspwpwf1  23874  fclscf  23912  flimfnfcls  23915  ustexsym  24103  ustuqtop4  24132  utop3cls  24139  utopreg  24140  ucnima  24168  ucncn  24172  metequiv2  24398  prdsxmslem2  24417  metcnpi3  24434  metustto  24441  metustid  24442  metustexhalf  24444  ngptgp  24524  xrsblre  24700  icccmp  24714  reconnlem1  24715  reconn  24717  opnreen  24720  metdsf  24737  metdscn  24745  mpomulcn  24758  fsumcn  24761  elcncf2  24783  cncfmet  24802  pcoass  24924  lmcau  25213  rrxdstprj1  25309  pmltpc  25351  ivthlem2  25353  ivthlem3  25354  ovollb2  25390  volsup  25457  ioombl1  25463  ioorf  25474  dyadss  25495  dyaddisjlem  25496  dyadmax  25499  volcn  25507  cncombf  25559  mbflimsup  25567  itg2const2  25642  iblss2  25707  cpnord  25837  dvmptfsum  25879  fta1g  26075  plydivex  26205  fta1  26216  aannenlem1  26236  ulmdvlem3  26311  advlogexp  26564  cxpmul2z  26600  atantayl2  26848  jensen  26899  isppw2  27025  lgsqr  27262  lgsqrmodndvds  27264  lgsdchrval  27265  lgsquad3  27298  2sqb  27343  dchrisumlem3  27402  pntrsumbnd2  27478  noinfbnd1lem5  27639  noetasuplem4  27648  noetainflem4  27652  noetalem1  27653  conway  27711  madebdayim  27799  madebdaylemlrcut  27810  negsprop  27941  mulscom  28042  absmuls  28146  bdayon  28173  remulscl  28353  tgjustf  28400  axsegcon  28854  axeuclidlem  28889  axcontlem9  28899  eengtrkg  28913  cusgrsize2inds  29381  pthdepisspth  29665  usgr2wlkneq  29686  crctcshwlkn0  29751  wpthswwlks2on  29891  clwwlkccatlem  29918  wwlksext2clwwlk  29986  umgr3v3e3cycl  30113  vdgn1frgrv2  30225  frgrwopreglem5  30250  frgrwopreg  30252  frgrhash2wsp  30261  numclwwlk1lem2fo  30287  vacn  30623  smcnlem  30626  0lno  30719  chocunii  31230  occl  31233  5oalem1  31583  3oalem2  31592  unoplin  31849  hmoplin  31871  lnconi  31962  kbass5  32049  mdslmd1lem1  32254  mdslmd1lem2  32255  mdsymlem2  32333  cdj1i  32362  opreu2reuALT  32406  unidifsnne  32465  disjabrex  32511  disjabrexf  32512  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  33140  archiabllem1  33147  archiabllem2a  33148  rlocval  33210  isarchiofld  33295  imaslmod  33324  lindfpropd  33353  unitprodclb  33360  elrspunidl  33399  dfufd2lem  33520  lvecdim0  33602  constrmon  33734  constrextdg2  33739  locfinreflem  33830  zarcmplem  33871  rge0scvg  33939  lmxrge0  33942  lmdvg  33943  qqhval2  33972  esumrnmpt2  34058  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  esumgect  34080  esumiun  34084  sigaclfu2  34111  sigainb  34126  insiga  34127  fiunelros  34164  measinblem  34210  measinb  34211  measdivcst  34214  measdivcstALTV  34215  omssubadd  34291  oddpwdc  34345  dstrvprob  34463  signsply0  34542  signstfvneq0  34563  bnj1408  35026  ptpconn  35220  sconnpi1  35226  resconn  35233  cvmliftmolem2  35269  cvmlift2lem12  35301  satfsschain  35351  satffunlem2lem1  35391  ifscgr  36032  cgrxfr  36043  outsideofeu  36119  linethru  36141  neibastop1  36347  dnicn  36480  irrdifflemf  37313  irrdiff  37314  fin2so  37601  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem28  37642  poimirlem31  37645  mblfinlem2  37652  mblfinlem3  37653  itg2addnclem  37665  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  ssbnd  37782  totbndbnd  37783  prtlem10  38858  lssats  39005  lkrlss  39088  lshpset2N  39112  2dim  39464  islvol5  39573  paddasslem11  39824  pexmidlem8N  39971  ltrnid  40129  idltrn  40144  trlator0  40165  trlnidatb  40171  cdlemf2  40556  cdlemg2cex  40585  tendodi1  40778  tendodi2  40779  diblss  41164  dihopelvalcpre  41242  dih1dimatlem  41323  dihglblem6  41334  primrootscoprmpow  42087  posbezout  42088  aks6d1c4  42112  sticksstones22  42156  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6lem5  42165  grpods  42182  unitscyglem3  42185  unitscyglem4  42186  remul01  42395  sn-subeu  42415  sn-0tie0  42439  prjspertr  42593  prjspersym  42595  0prjspnrel  42615  mzpsubst  42736  mzpcompact2lem  42739  eldioph2  42750  eldioph2b  42751  diophren  42801  pell14qrexpcl  42855  elpell1qr2  42860  monotoddzzfi  42931  acongtr  42967  acongrep  42969  jm2.19lem4  42981  jm2.26a  42989  jm2.26lem3  42990  jm2.26  42991  isnumbasgrplem2  43093  mendassa  43179  omord2lim  43289  cantnftermord  43309  tfsconcatfv1  43328  tfsconcatfv2  43329  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddgeoa  43383  clsk3nimkb  44029  prmunb2  44300  4an4132  44489  fiiuncl  45059  ssinc  45081  ssdec  45082  supxrgelem  45333  infxr  45363  cvgcaule  45487  mullimc  45614  mullimcf  45621  neglimc  45645  climleltrp  45674  climisp  45744  limsupresxr  45764  liminfresxr  45765  liminflimsupclim  45805  xlimliminflimsup  45860  icccncfext  45885  cncfiooicclem1  45891  fprodcncf  45898  dvnprodlem3  45946  iblcncfioo  45976  itgspltprt  45977  stoweidlem7  46005  stoweidlem28  46026  stoweidlem34  46032  stoweidlem48  46046  stoweidlem52  46050  wallispilem3  46065  fourierdlem12  46117  fourierdlem38  46143  fourierdlem39  46144  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem65  46169  fourierdlem73  46177  fourierdlem76  46180  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  sge0f1o  46380  sge0le  46405  sge0reuz  46445  ismeannd  46465  isomenndlem  46528  hoicvr  46546  hoidmvle  46598  smflimlem2  46770  smflimmpt  46808  fsupdm  46840  finfdm  46844  imasetpreimafvbijlemf1  47405  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  isubgr3stgrlem6  47970  rrxlinec  48725  iccdisj  48886  upfval  49165  fullthinc  49439