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  7210  poseq  8100  oeeui  8530  oaabs2  8577  naddssim  8613  omxpenlem  9006  findcard3  9183  wemappo  9454  acndom2  9964  infpwfien  9972  sornom  10187  isf32lem2  10264  isf32lem4  10266  fin1a2lem11  10320  pwfseq  10575  gchina  10610  inttsk  10685  inar1  10686  prlem936  10958  mulcmpblnr  10982  00id  11308  mul02lem1  11309  addrid  11313  cnegex  11314  negeu  11370  add20  11649  ltmul12a  11997  lediv12a  12035  cru  12137  qextltlem  13117  xmullem  13179  xlemul1a  13203  ixxss12  13281  ioodisj  13398  elfz0fzfz0  13549  fsuppmapnn0fz  13919  seqf1o  13966  mulexpz  14025  leexp1a  14098  seqcoll  14387  swrdswrdlem  14627  pfxccatin12lem3  14655  abs3lem  15262  cau3lem  15278  climcau  15594  sumeq2ii  15616  climcndslem1  15772  climcndslem2  15773  geomulcvg  15799  mertenslem1  15807  mertenslem2  15808  mertens  15809  prodeq2ii  15834  prodmolem2  15858  bitsfzo  16362  sadadd2lem2  16377  dvdsmulgcd  16483  qredeu  16585  pc2dvds  16807  pcz  16809  ramcl  16957  firest  17352  mreexexlemd  17567  isacs2  17576  iscatd2  17604  ipodrsima  18464  mrelatlub  18485  mgmhmeql  18641  sgrppropd  18656  mndpropd  18684  mhmeql  18751  mhmid  18993  mhmmnd  18994  issubg4  19075  cycsubm  19131  cycsubmcom  19133  gasubg  19231  symgextf  19346  pmtr3ncom  19404  gexdvds  19513  oddvdssubg  19784  imasabl  19805  cyggeninv  19812  cyggenod  19813  submomnd  20061  issrg  20123  dvdsrmul1  20305  unitgrp  20319  cntzsubrng  20500  cntzsubr  20539  islmhm2  20990  lmhmeql  21007  lbspropd  21051  lssacsex  21099  rngqiprngimfo  21256  psgndiflemA  21556  isphl  21583  ocvocv  21626  lindfmm  21782  issubassa2  21848  mplbas2  21997  scmatmats  22455  smatvscl  22468  mdetdiag  22543  m2cpmfo  22700  pmatcollpw3fi1lem1  22730  pm2mpf1  22743  pm2mpghm  22760  fvmptnn04if  22793  chfacfscmulfsupp  22803  chfacfpmmulfsupp  22807  neissex  23071  neiptoptop  23075  neiptopnei  23076  restbas  23102  tgrest  23103  restopnb  23119  cnpco  23211  isreg2  23321  iunconn  23372  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  2ndcsep  23403  dislly  23441  kgencn2  23501  ptbasfi  23525  txhaus  23591  txkgen  23596  txconn  23633  qtopcn  23658  regr1lem2  23684  kqnrmlem1  23687  kqnrmlem2  23688  trfbas2  23787  trfil2  23831  flimcf  23926  hauspwpwf1  23931  fclscf  23969  flimfnfcls  23972  ustexsym  24160  ustuqtop4  24188  utop3cls  24195  utopreg  24196  ucnima  24224  ucncn  24228  metequiv2  24454  prdsxmslem2  24473  metcnpi3  24490  metustto  24497  metustid  24498  metustexhalf  24500  ngptgp  24580  xrsblre  24756  icccmp  24770  reconnlem1  24771  reconn  24773  opnreen  24776  metdsf  24793  metdscn  24801  mpomulcn  24814  fsumcn  24817  elcncf2  24839  cncfmet  24858  pcoass  24980  lmcau  25269  rrxdstprj1  25365  pmltpc  25407  ivthlem2  25409  ivthlem3  25410  ovollb2  25446  volsup  25513  ioombl1  25519  ioorf  25530  dyadss  25551  dyaddisjlem  25552  dyadmax  25555  volcn  25563  cncombf  25615  mbflimsup  25623  itg2const2  25698  iblss2  25763  cpnord  25893  dvmptfsum  25935  fta1g  26131  plydivex  26261  fta1  26272  aannenlem1  26292  ulmdvlem3  26367  advlogexp  26620  cxpmul2z  26656  atantayl2  26904  jensen  26955  isppw2  27081  lgsqr  27318  lgsqrmodndvds  27320  lgsdchrval  27321  lgsquad3  27354  2sqb  27399  dchrisumlem3  27458  pntrsumbnd2  27534  noinfbnd1lem5  27695  noetasuplem4  27704  noetainflem4  27708  noetalem1  27709  conway  27775  eqcuts3  27800  madebdayim  27884  madebdaylemlrcut  27895  negsprop  28031  mulscom  28135  absmuls  28240  bdayons  28272  addonbday  28275  bdayfinbndlem1  28463  remulscl  28498  tgjustf  28545  axsegcon  29000  axeuclidlem  29035  axcontlem9  29045  eengtrkg  29059  cusgrsize2inds  29527  pthdepisspth  29808  usgr2wlkneq  29829  crctcshwlkn0  29894  wpthswwlks2on  30037  clwwlkccatlem  30064  wwlksext2clwwlk  30132  umgr3v3e3cycl  30259  vdgn1frgrv2  30371  frgrwopreglem5  30396  frgrwopreg  30398  frgrhash2wsp  30407  numclwwlk1lem2fo  30433  vacn  30769  smcnlem  30772  0lno  30865  chocunii  31376  occl  31379  5oalem1  31729  3oalem2  31738  unoplin  31995  hmoplin  32017  lnconi  32108  kbass5  32195  mdslmd1lem1  32400  mdslmd1lem2  32401  mdsymlem2  32479  cdj1i  32508  opreu2reuALT  32551  unidifsnne  32611  disjabrex  32657  disjabrexf  32658  acunirnmpt  32737  fgreu  32750  suppovss  32760  xrge0infss  32840  xrofsup  32847  fsumiunle  32910  sgnmul  32916  sgnsub  32918  mgcf1o  33085  xrge0addgt0  33099  fzto1st1  33184  cyc3genpm  33234  cycpmgcl  33235  submarchi  33268  archiabllem1  33275  archiabllem2a  33276  isarchiofld  33281  rlocval  33341  imaslmod  33434  lindfpropd  33463  unitprodclb  33470  elrspunidl  33509  dfufd2lem  33630  mplmulmvr  33704  lvecdim0  33763  constrmon  33901  constrextdg2  33906  locfinreflem  33997  zarcmplem  34038  rge0scvg  34106  lmxrge0  34109  lmdvg  34110  qqhval2  34139  esumrnmpt2  34225  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  esumgect  34247  esumiun  34251  sigaclfu2  34278  sigainb  34293  insiga  34294  fiunelros  34331  measinblem  34377  measinb  34378  measdivcst  34381  measdivcstALTV  34382  omssubadd  34457  oddpwdc  34511  dstrvprob  34629  signsply0  34708  signstfvneq0  34729  bnj1408  35192  ptpconn  35427  sconnpi1  35433  resconn  35440  cvmliftmolem2  35476  cvmlift2lem12  35508  satfsschain  35558  satffunlem2lem1  35598  ifscgr  36238  cgrxfr  36249  outsideofeu  36325  linethru  36347  neibastop1  36553  dnicn  36692  irrdifflemf  37530  irrdiff  37531  fin2so  37808  matunitlindflem1  37817  matunitlindflem2  37818  poimirlem28  37849  poimirlem31  37852  mblfinlem2  37859  mblfinlem3  37860  itg2addnclem  37872  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  ssbnd  37989  totbndbnd  37990  prtlem10  39125  lssats  39272  lkrlss  39355  lshpset2N  39379  2dim  39730  islvol5  39839  paddasslem11  40090  pexmidlem8N  40237  ltrnid  40395  idltrn  40410  trlator0  40431  trlnidatb  40437  cdlemf2  40822  cdlemg2cex  40851  tendodi1  41044  tendodi2  41045  diblss  41430  dihopelvalcpre  41508  dih1dimatlem  41589  dihglblem6  41600  primrootscoprmpow  42353  posbezout  42354  aks6d1c4  42378  sticksstones22  42422  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6lem5  42431  grpods  42448  unitscyglem3  42451  unitscyglem4  42452  remul01  42662  sn-subeu  42682  sn-0tie0  42706  prjspertr  42848  prjspersym  42850  0prjspnrel  42870  mzpsubst  42990  mzpcompact2lem  42993  eldioph2  43004  eldioph2b  43005  diophren  43055  pell14qrexpcl  43109  elpell1qr2  43114  monotoddzzfi  43184  acongtr  43220  acongrep  43222  jm2.19lem4  43234  jm2.26a  43242  jm2.26lem3  43243  jm2.26  43244  isnumbasgrplem2  43346  mendassa  43432  omord2lim  43542  cantnftermord  43562  tfsconcatfv1  43581  tfsconcatfv2  43582  naddcnffo  43606  naddcnfcom  43608  naddcnfid1  43609  naddgeoa  43636  clsk3nimkb  44281  prmunb2  44552  4an4132  44740  fiiuncl  45310  ssinc  45331  ssdec  45332  supxrgelem  45582  infxr  45611  cvgcaule  45735  mullimc  45862  mullimcf  45869  neglimc  45891  climleltrp  45920  climisp  45990  limsupresxr  46010  liminfresxr  46011  liminflimsupclim  46051  xlimliminflimsup  46106  icccncfext  46131  cncfiooicclem1  46137  fprodcncf  46144  dvnprodlem3  46192  iblcncfioo  46222  itgspltprt  46223  stoweidlem7  46251  stoweidlem28  46272  stoweidlem34  46278  stoweidlem48  46292  stoweidlem52  46296  wallispilem3  46311  fourierdlem12  46363  fourierdlem38  46389  fourierdlem39  46390  fourierdlem42  46393  fourierdlem46  46396  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem65  46415  fourierdlem73  46423  fourierdlem76  46426  fourierdlem87  46437  fourierdlem103  46453  fourierdlem104  46454  sge0f1o  46626  sge0le  46651  sge0reuz  46691  ismeannd  46711  isomenndlem  46774  hoicvr  46792  hoidmvle  46844  smflimlem2  47016  smflimmpt  47054  fsupdm  47086  finfdm  47090  imasetpreimafvbijlemf1  47650  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbnd  48055  isubgr3stgrlem6  48217  rrxlinec  48982  iccdisj  49143  upfval  49421  fullthinc  49695