MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simplll Structured version   Visualization version   GIF version

Theorem simplll 771
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
StepHypRef Expression
1 id 22 . 2 (𝜑𝜑)
21ad3antrrr 726 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  f1imass  7019  oeeui  8221  oaabs2  8265  omxpenlem  8610  acndom2  9472  infpwfien  9480  sornom  9691  isf32lem2  9768  isf32lem4  9770  fin1a2lem11  9824  pwfseq  10078  gchina  10113  inttsk  10188  inar1  10189  prlem936  10461  mulcmpblnr  10485  00id  10807  mul02lem1  10808  addid1  10812  cnegex  10813  negeu  10868  add20  11144  ltmul12a  11488  lediv12a  11525  fiminreOLD  11582  cru  11622  qextltlem  12588  xmullem  12650  xlemul1a  12674  ixxss12  12751  ioodisj  12861  elfz0fzfz0  13005  fsuppmapnn0fz  13357  seqf1o  13404  mulexpz  13462  leexp1a  13532  seqcoll  13815  swrdswrdlem  14059  pfxccatin12lem3  14087  abs3lem  14691  cau3lem  14707  climcau  15020  sumeq2ii  15043  climcndslem1  15197  climcndslem2  15198  geomulcvg  15225  mertenslem1  15233  mertenslem2  15234  mertens  15235  prodeq2ii  15260  prodmolem2  15282  bitsfzo  15777  sadadd2lem2  15792  dvdsmulgcd  15898  qredeu  15995  pc2dvds  16208  pcz  16210  ramcl  16358  firest  16699  mreexexlemd  16908  isacs2  16917  iscatd2  16945  ipodrsima  17768  mrelatlub  17789  mndpropd  17927  mhmeql  17976  mhmid  18153  mhmmnd  18154  issubg4  18231  cycsubm  18278  cycsubmcom  18280  gasubg  18365  symgextf  18468  pmtr3ncom  18526  gexdvds  18632  oddvdssubg  18898  cyggeninv  18925  cyggenod  18926  issrg  19180  dvdsrmul1  19326  unitgrp  19340  cntzsubr  19491  islmhm2  19733  lmhmeql  19750  lbspropd  19794  lssacsex  19839  issubassa2  20043  mplbas2  20172  psgndiflemA  20664  isphl  20691  ocvocv  20734  lindfmm  20890  scmatmats  21039  smatvscl  21052  mdetdiag  21127  m2cpmfo  21283  pmatcollpw3fi1lem1  21313  pm2mpf1  21326  pm2mpghm  21343  fvmptnn04if  21376  chfacfscmulfsupp  21386  chfacfpmmulfsupp  21390  neissex  21654  neiptoptop  21658  neiptopnei  21659  restbas  21685  tgrest  21686  restopnb  21702  cnpco  21794  isreg2  21904  iunconn  21955  1stcrest  21980  2ndcctbss  21982  2ndcomap  21985  2ndcsep  21986  dislly  22024  kgencn2  22084  ptbasfi  22108  txhaus  22174  txkgen  22179  txconn  22216  qtopcn  22241  regr1lem2  22267  kqnrmlem1  22270  kqnrmlem2  22271  trfbas2  22370  trfil2  22414  flimcf  22509  hauspwpwf1  22514  fclscf  22552  flimfnfcls  22555  ustexsym  22742  ustuqtop4  22771  utop3cls  22778  utopreg  22779  ucnima  22808  ucncn  22812  metequiv2  23038  prdsxmslem2  23057  metcnpi3  23074  metustto  23081  metustid  23082  metustexhalf  23084  ngptgp  23163  xrsblre  23337  icccmp  23351  reconnlem1  23352  reconn  23354  opnreen  23357  metdsf  23374  metdscn  23382  fsumcn  23396  elcncf2  23416  cncfmet  23434  pcoass  23546  lmcau  23834  rrxdstprj1  23930  pmltpc  23969  ivthlem2  23971  ivthlem3  23972  ovollb2  24008  volsup  24075  ioombl1  24081  ioorf  24092  dyadss  24113  dyaddisjlem  24114  dyadmax  24117  volcn  24125  cncombf  24177  mbflimsup  24185  itg2const2  24260  iblss2  24324  cpnord  24450  dvmptfsum  24490  fta1g  24679  plydivex  24804  fta1  24815  aannenlem1  24835  ulmdvlem3  24908  advlogexp  25154  cxpmul2z  25190  atantayl2  25432  jensen  25483  isppw2  25609  lgsqr  25844  lgsqrmodndvds  25846  lgsdchrval  25847  lgsquad3  25880  2sqb  25925  dchrisumlem3  25984  pntrsumbnd2  26060  tgjustf  26176  axsegcon  26630  axeuclidlem  26665  axcontlem9  26675  eengtrkg  26689  cusgrsize2inds  27152  pthdepisspth  27433  usgr2wlkneq  27454  crctcshwlkn0  27516  wpthswwlks2on  27657  clwwlkccatlem  27684  wwlksext2clwwlk  27753  umgr3v3e3cycl  27880  vdgn1frgrv2  27992  frgrwopreglem5  28017  frgrwopreg  28019  frgrhash2wsp  28028  numclwwlk1lem2fo  28054  vacn  28388  smcnlem  28391  0lno  28484  chocunii  28995  occl  28998  5oalem1  29348  3oalem2  29357  unoplin  29614  hmoplin  29636  lnconi  29727  kbass5  29814  mdslmd1lem1  30019  mdslmd1lem2  30020  mdsymlem2  30098  cdj1i  30127  opreu2reuALT  30157  unidifsnne  30213  disjabrex  30250  disjabrexf  30251  acunirnmpt  30322  fgreu  30335  suppovss  30344  xrge0infss  30400  xrofsup  30408  fsumiunle  30462  xrge0addgt0  30595  submomnd  30628  fzto1st1  30661  cyc3genpm  30711  cycpmgcl  30712  submarchi  30732  archiabllem1  30739  archiabllem2a  30740  isarchiofld  30807  imaslmod  30839  lindfpropd  30859  lvecdim0  30894  locfinreflem  30993  rge0scvg  31081  lmxrge0  31084  lmdvg  31085  qqhval2  31112  esumrnmpt2  31216  esumfsup  31218  esumpcvgval  31226  esumcvg  31234  esumgect  31238  esumiun  31242  sigaclfu2  31269  sigainb  31284  insiga  31285  fiunelros  31322  measinblem  31368  measinb  31369  measdivcst  31372  measdivcstALTV  31373  omssubadd  31447  oddpwdc  31501  dstrvprob  31618  sgnmul  31689  sgnsub  31691  signsply0  31710  signstfvneq0  31731  bnj1408  32195  ptpconn  32367  sconnpi1  32373  resconn  32380  cvmliftmolem2  32416  cvmlift2lem12  32448  satfsschain  32498  satffunlem2lem1  32538  poseq  32982  noetalem3  33106  noetalem5  33108  conway  33151  ifscgr  33392  cgrxfr  33403  outsideofeu  33479  linethru  33501  neibastop1  33594  dnicn  33718  fin2so  34749  matunitlindflem1  34758  matunitlindflem2  34759  poimirlem28  34790  poimirlem31  34793  mblfinlem2  34800  mblfinlem3  34801  itg2addnclem  34813  ftc1anclem7  34843  ftc1anclem8  34844  ftc1anc  34845  ssbnd  34937  totbndbnd  34938  prtlem10  35871  lssats  36018  lkrlss  36101  lshpset2N  36125  2dim  36476  islvol5  36585  paddasslem11  36836  pexmidlem8N  36983  ltrnid  37141  idltrn  37156  trlator0  37177  trlnidatb  37183  cdlemf2  37568  cdlemg2cex  37597  tendodi1  37790  tendodi2  37791  diblss  38176  dihopelvalcpre  38254  dih1dimatlem  38335  dihglblem6  38346  remul01  39105  prjspertr  39123  prjspersym  39125  0prjspnrel  39137  mzpsubst  39213  mzpcompact2lem  39216  eldioph2  39227  eldioph2b  39228  diophren  39278  pell14qrexpcl  39332  elpell1qr2  39337  monotoddzzfi  39407  acongtr  39443  acongrep  39445  jm2.19lem4  39457  jm2.26a  39465  jm2.26lem3  39466  jm2.26  39467  isnumbasgrplem2  39572  mendassa  39662  clsk3nimkb  40258  prmunb2  40511  4an4132  40701  fiiuncl  41195  ssinc  41221  ssdec  41222  supxrgelem  41473  infxr  41503  mullimc  41765  mullimcf  41772  neglimc  41796  climleltrp  41825  climisp  41895  limsupresxr  41915  liminfresxr  41916  liminflimsupclim  41956  xlimliminflimsup  42011  icccncfext  42038  cncfiooicclem1  42044  fprodcncf  42052  dvnprodlem3  42101  iblcncfioo  42131  itgspltprt  42132  stoweidlem7  42161  stoweidlem28  42182  stoweidlem34  42188  stoweidlem48  42202  stoweidlem52  42206  wallispilem3  42221  fourierdlem12  42273  fourierdlem38  42299  fourierdlem39  42300  fourierdlem42  42303  fourierdlem46  42306  fourierdlem48  42308  fourierdlem49  42309  fourierdlem50  42310  fourierdlem51  42311  fourierdlem65  42325  fourierdlem73  42333  fourierdlem76  42336  fourierdlem87  42347  fourierdlem103  42363  fourierdlem104  42364  sge0f1o  42533  sge0le  42558  sge0reuz  42598  ismeannd  42618  isomenndlem  42681  hoicvr  42699  hoidmvle  42751  smflimlem2  42917  smflimmpt  42953  nnsum4primeseven  43800  nnsum4primesevenALTV  43801  bgoldbtbndlem2  43806  bgoldbtbndlem3  43807  bgoldbtbnd  43809  isomuspgrlem2  43833  mgmhmeql  43905  rrxlinec  44558
  Copyright terms: Public domain W3C validator