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 729	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  f1imass  7020  oeeui  8244  oaabs2  8288  omxpenlem  8652  wemappo  9059  acndom2  9527  infpwfien  9535  sornom  9750  isf32lem2  9827  isf32lem4  9829  fin1a2lem11  9883  pwfseq  10137  gchina  10172  inttsk  10247  inar1  10248  prlem936  10520  mulcmpblnr  10544  00id  10866  mul02lem1  10867  addid1  10871  cnegex  10872  negeu  10927  add20  11203  ltmul12a  11547  lediv12a  11584  cru  11679  qextltlem  12649  xmullem  12711  xlemul1a  12735  ixxss12  12812  ioodisj  12927  elfz0fzfz0  13074  fsuppmapnn0fz  13426  seqf1o  13474  mulexpz  13532  leexp1a  13602  seqcoll  13887  swrdswrdlem  14126  pfxccatin12lem3  14154  abs3lem  14759  cau3lem  14775  climcau  15088  sumeq2ii  15111  climcndslem1  15265  climcndslem2  15266  geomulcvg  15293  mertenslem1  15301  mertenslem2  15302  mertens  15303  prodeq2ii  15328  prodmolem2  15350  bitsfzo  15847  sadadd2lem2  15862  dvdsmulgcd  15970  qredeu  16068  pc2dvds  16284  pcz  16286  ramcl  16434  firest  16778  mreexexlemd  16987  isacs2  16996  iscatd2  17024  ipodrsima  17855  mrelatlub  17876  mndpropd  18016  mhmeql  18070  mhmid  18301  mhmmnd  18302  issubg4  18379  cycsubm  18426  cycsubmcom  18428  gasubg  18513  symgextf  18626  pmtr3ncom  18684  gexdvds  18790  oddvdssubg  19057  cyggeninv  19084  cyggenod  19085  issrg  19339  dvdsrmul1  19488  unitgrp  19502  cntzsubr  19650  islmhm2  19892  lmhmeql  19909  lbspropd  19953  lssacsex  19998  psgndiflemA  20380  isphl  20407  ocvocv  20450  lindfmm  20606  issubassa2  20669  mplbas2  20816  scmatmats  21225  smatvscl  21238  mdetdiag  21313  m2cpmfo  21470  pmatcollpw3fi1lem1  21500  pm2mpf1  21513  pm2mpghm  21530  fvmptnn04if  21563  chfacfscmulfsupp  21573  chfacfpmmulfsupp  21577  neissex  21841  neiptoptop  21845  neiptopnei  21846  restbas  21872  tgrest  21873  restopnb  21889  cnpco  21981  isreg2  22091  iunconn  22142  1stcrest  22167  2ndcctbss  22169  2ndcomap  22172  2ndcsep  22173  dislly  22211  kgencn2  22271  ptbasfi  22295  txhaus  22361  txkgen  22366  txconn  22403  qtopcn  22428  regr1lem2  22454  kqnrmlem1  22457  kqnrmlem2  22458  trfbas2  22557  trfil2  22601  flimcf  22696  hauspwpwf1  22701  fclscf  22739  flimfnfcls  22742  ustexsym  22930  ustuqtop4  22959  utop3cls  22966  utopreg  22967  ucnima  22996  ucncn  23000  metequiv2  23226  prdsxmslem2  23245  metcnpi3  23262  metustto  23269  metustid  23270  metustexhalf  23272  ngptgp  23352  xrsblre  23526  icccmp  23540  reconnlem1  23541  reconn  23543  opnreen  23546  metdsf  23563  metdscn  23571  fsumcn  23585  elcncf2  23605  cncfmet  23624  pcoass  23739  lmcau  24027  rrxdstprj1  24123  pmltpc  24164  ivthlem2  24166  ivthlem3  24167  ovollb2  24203  volsup  24270  ioombl1  24276  ioorf  24287  dyadss  24308  dyaddisjlem  24309  dyadmax  24312  volcn  24320  cncombf  24372  mbflimsup  24380  itg2const2  24455  iblss2  24519  cpnord  24648  dvmptfsum  24688  fta1g  24881  plydivex  25006  fta1  25017  aannenlem1  25037  ulmdvlem3  25110  advlogexp  25359  cxpmul2z  25395  atantayl2  25637  jensen  25687  isppw2  25813  lgsqr  26048  lgsqrmodndvds  26050  lgsdchrval  26051  lgsquad3  26084  2sqb  26129  dchrisumlem3  26188  pntrsumbnd2  26264  tgjustf  26380  axsegcon  26834  axeuclidlem  26869  axcontlem9  26879  eengtrkg  26893  cusgrsize2inds  27356  pthdepisspth  27637  usgr2wlkneq  27658  crctcshwlkn0  27720  wpthswwlks2on  27860  clwwlkccatlem  27887  wwlksext2clwwlk  27955  umgr3v3e3cycl  28082  vdgn1frgrv2  28194  frgrwopreglem5  28219  frgrwopreg  28221  frgrhash2wsp  28230  numclwwlk1lem2fo  28256  vacn  28590  smcnlem  28593  0lno  28686  chocunii  29197  occl  29200  5oalem1  29550  3oalem2  29559  unoplin  29816  hmoplin  29838  lnconi  29929  kbass5  30016  mdslmd1lem1  30221  mdslmd1lem2  30222  mdsymlem2  30300  cdj1i  30329  opreu2reuALT  30360  unidifsnne  30420  disjabrex  30457  disjabrexf  30458  acunirnmpt  30533  fgreu  30546  suppovss  30554  xrge0infss  30620  xrofsup  30627  fsumiunle  30680  mgcf1o  30820  xrge0addgt0  30839  submomnd  30875  fzto1st1  30908  cyc3genpm  30958  cycpmgcl  30959  submarchi  30979  archiabllem1  30986  archiabllem2a  30987  isarchiofld  31055  imaslmod  31087  lindfpropd  31110  elrspunidl  31140  lvecdim0  31224  locfinreflem  31324  zarcmplem  31365  rge0scvg  31433  lmxrge0  31436  lmdvg  31437  qqhval2  31464  esumrnmpt2  31568  esumfsup  31570  esumpcvgval  31578  esumcvg  31586  esumgect  31590  esumiun  31594  sigaclfu2  31621  sigainb  31636  insiga  31637  fiunelros  31674  measinblem  31720  measinb  31721  measdivcst  31724  measdivcstALTV  31725  omssubadd  31799  oddpwdc  31853  dstrvprob  31970  sgnmul  32041  sgnsub  32043  signsply0  32062  signstfvneq0  32083  bnj1408  32549  ptpconn  32724  sconnpi1  32730  resconn  32737  cvmliftmolem2  32773  cvmlift2lem12  32805  satfsschain  32855  satffunlem2lem1  32895  poseq  33370  naddssim  33435  noinfbnd1lem5  33528  noetasuplem4  33537  noetainflem4  33541  noetalem1  33542  conway  33589  madebdaylemlrcut  33671  ifscgr  33930  cgrxfr  33941  outsideofeu  34017  linethru  34039  neibastop1  34132  dnicn  34256  irrdifflemf  35054  irrdiff  35055  fin2so  35359  matunitlindflem1  35368  matunitlindflem2  35369  poimirlem28  35400  poimirlem31  35403  mblfinlem2  35410  mblfinlem3  35411  itg2addnclem  35423  ftc1anclem7  35451  ftc1anclem8  35452  ftc1anc  35453  ssbnd  35541  totbndbnd  35542  prtlem10  36476  lssats  36623  lkrlss  36706  lshpset2N  36730  2dim  37081  islvol5  37190  paddasslem11  37441  pexmidlem8N  37588  ltrnid  37746  idltrn  37761  trlator0  37782  trlnidatb  37788  cdlemf2  38173  cdlemg2cex  38202  tendodi1  38395  tendodi2  38396  diblss  38781  dihopelvalcpre  38859  dih1dimatlem  38940  dihglblem6  38951  remul01  39932  sn-subeu  39950  sn-0tie0  39963  itrere  39978  retire  39979  prjspertr  39986  prjspersym  39988  0prjspnrel  40006  mzpsubst  40107  mzpcompact2lem  40110  eldioph2  40121  eldioph2b  40122  diophren  40172  pell14qrexpcl  40226  elpell1qr2  40231  monotoddzzfi  40301  acongtr  40337  acongrep  40339  jm2.19lem4  40351  jm2.26a  40359  jm2.26lem3  40360  jm2.26  40361  isnumbasgrplem2  40466  mendassa  40556  clsk3nimkb  41161  prmunb2  41433  4an4132  41623  fiiuncl  42117  ssinc  42141  ssdec  42142  supxrgelem  42382  infxr  42412  mullimc  42669  mullimcf  42676  neglimc  42700  climleltrp  42729  climisp  42799  limsupresxr  42819  liminfresxr  42820  liminflimsupclim  42860  xlimliminflimsup  42915  icccncfext  42940  cncfiooicclem1  42946  fprodcncf  42953  dvnprodlem3  43001  iblcncfioo  43031  itgspltprt  43032  stoweidlem7  43060  stoweidlem28  43081  stoweidlem34  43087  stoweidlem48  43101  stoweidlem52  43105  wallispilem3  43120  fourierdlem12  43172  fourierdlem38  43198  fourierdlem39  43199  fourierdlem42  43202  fourierdlem46  43205  fourierdlem48  43207  fourierdlem49  43208  fourierdlem50  43209  fourierdlem51  43210  fourierdlem65  43224  fourierdlem73  43232  fourierdlem76  43235  fourierdlem87  43246  fourierdlem103  43262  fourierdlem104  43263  sge0f1o  43432  sge0le  43457  sge0reuz  43497  ismeannd  43517  isomenndlem  43580  hoicvr  43598  hoidmvle  43650  smflimlem2  43816  smflimmpt  43852  imasetpreimafvbijlemf1  44348  nnsum4primeseven  44744  nnsum4primesevenALTV  44745  bgoldbtbndlem2  44750  bgoldbtbndlem3  44751  bgoldbtbnd  44753  isomuspgrlem2  44777  mgmhmeql  44849  rrxlinec  45574  iccdisj  45644