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

Theorem simplll 813
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 766 1 ((((𝜑𝜓) ∧ 𝜒) ∧ 𝜃) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  simp-4l  823  adant423OLD  840  f1imass  6561  oeeui  7727  oaabs2  7770  omxpenlem  8102  cantnfle  8606  acndom2  8915  infpwfien  8923  sornom  9137  isf32lem2  9214  isf32lem4  9216  fin1a2lem11  9270  ttukeylem5  9373  pwfseq  9524  gchina  9559  inttsk  9634  inar1  9635  prlem936  9907  mulcmpblnr  9930  00id  10249  mul02lem1  10250  addid1  10254  cnegex  10255  negeu  10309  add20  10578  ltmul12a  10917  lediv12a  10954  fiminre  11010  cru  11050  qextltlem  12071  xmullem  12132  xlemul1a  12156  ixxss12  12233  ioodisj  12340  elfz0fzfz0  12483  fsuppmapnn0fz  12836  seqf1o  12882  mulexpz  12940  leexp1a  12959  seqcoll  13286  swrdswrdlem  13505  abs3lem  14122  cau3lem  14138  climcau  14445  sumeq2ii  14467  summolem2  14491  climcndslem1  14625  climcndslem2  14626  geomulcvg  14651  mertenslem1  14660  mertenslem2  14661  mertens  14662  prodeq2ii  14687  prodmolem2  14709  bitsfzo  15204  sadadd2lem2  15219  dvdsmulgcd  15321  qredeu  15419  pc2dvds  15630  pcz  15632  ramcl  15780  firest  16140  mreexexlemd  16351  isacs2  16361  iscatd2  16389  ipodrsima  17212  mrelatlub  17233  mndpropd  17363  mhmeql  17411  isgrpinv  17519  mhmid  17583  mhmmnd  17584  issubg4  17660  gasubg  17781  symgextf  17883  pmtr3ncom  17941  gexdvds  18045  oddvdssubg  18304  cyggeninv  18331  cyggenod  18332  issrg  18553  dvdsrmul1  18699  unitgrp  18713  cntzsubr  18860  islmhm2  19086  lmhmeql  19103  lbspropd  19147  lssacsex  19192  issubassa2  19393  mplbas2  19518  psgndiflemA  19995  isphl  20021  ocvocv  20063  lindfmm  20214  scmatmats  20365  smatvscl  20378  mdetdiag  20453  m2cpmfo  20609  pmatcollpw3fi1lem1  20639  pm2mpf1  20652  pm2mpghm  20669  fvmptnn04if  20702  chfacfscmulfsupp  20712  chfacfpmmulfsupp  20716  neissex  20979  neiptoptop  20983  neiptopnei  20984  restbas  21010  tgrest  21011  restopnb  21027  cnpco  21119  isnrm3  21211  isreg2  21229  iunconn  21279  1stcrest  21304  2ndcctbss  21306  2ndcomap  21309  2ndcsep  21310  dislly  21348  kgencn2  21408  ptbasfi  21432  txhaus  21498  txkgen  21503  txconn  21540  qtopcn  21565  regr1lem2  21591  kqnrmlem1  21594  kqnrmlem2  21595  trfbas2  21694  trfil2  21738  flimcf  21833  hauspwpwf1  21838  fclscf  21876  flimfnfcls  21879  cnextcn  21918  ustexsym  22066  ustex2sym  22067  ustex3sym  22068  ustuqtop4  22095  utop3cls  22102  utopreg  22103  ucnima  22132  ucncn  22136  fmucnd  22143  metequiv2  22362  prdsxmslem2  22381  metcnpi3  22398  metustto  22405  metustid  22406  metustexhalf  22408  ngptgp  22487  xrsblre  22661  icccmp  22675  reconnlem1  22676  reconn  22678  opnreen  22681  metdsf  22698  metdscn  22706  fsumcn  22720  elcncf2  22740  cncfmet  22758  pcoass  22870  lmcau  23157  rrxdstprj1  23238  pmltpc  23265  ivthlem2  23267  ivthlem3  23268  ovollb2  23303  volsup  23370  ioombl1  23376  ioorf  23387  dyadss  23408  dyaddisjlem  23409  dyadmax  23412  volcn  23420  cncombf  23470  mbflimsup  23478  itg2const2  23553  iblss2  23617  cpnord  23743  dvmptfsum  23783  fta1g  23972  plydivex  24097  fta1  24108  aannenlem1  24128  ulmdvlem3  24201  abelthlem8  24238  pilem3  24252  advlogexp  24446  cxpmul2z  24482  atantayl2  24710  jensen  24760  isppw2  24886  lgsqr  25121  lgsqrmodndvds  25123  lgsdchrval  25124  lgsquad3  25157  2sqb  25202  dchrisumlem3  25225  rpvmasum2  25246  mulog2sumlem2  25269  pntrsumbnd2  25301  f1otrg  25796  f1otrge  25797  axsegcon  25852  axeuclidlem  25887  axcontlem9  25897  eengtrkg  25910  cusgrsize2inds  26405  pthdepisspth  26687  usgr2wlkneq  26708  crctcshwlkn0  26769  wpthswwlks2on  26927  umgr3v3e3cycl  27162  vdgn1frgrv2  27276  frgrwopreglem5  27301  frgrwopreg  27303  frgrhash2wsp  27312  numclwlk1lem2fo  27348  vacn  27677  smcnlem  27680  0lno  27773  chocunii  28288  occl  28291  5oalem1  28641  3oalem2  28650  unoplin  28907  hmoplin  28929  lnconi  29020  kbass5  29107  mdslmd1lem1  29312  mdslmd1lem2  29313  mdsymlem2  29391  cdj1i  29420  disjabrex  29521  disjabrexf  29522  acunirnmpt  29587  fgreu  29599  xrge0infss  29653  xrofsup  29661  fsumiunle  29703  xrge0addgt0  29819  submomnd  29838  submarchi  29868  archiabllem1  29875  archiabllem2a  29876  isarchiofld  29945  locfinreflem  30035  rge0scvg  30123  lmxrge0  30126  lmdvg  30127  qqhval2  30154  esumrnmpt2  30258  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  esumgect  30280  esumiun  30284  sigaclfu2  30312  sigainb  30327  insiga  30328  fiunelros  30365  measinblem  30411  measinb  30412  measdivcstOLD  30415  measdivcst  30416  omssubadd  30490  oddpwdc  30544  dstrvprob  30661  sgnmul  30732  sgnsub  30734  signsply0  30756  signstfvneq0  30777  bnj1408  31230  ptpconn  31341  sconnpi1  31347  resconn  31354  cvmliftmolem2  31390  cvmlift2lem12  31422  poseq  31878  noetalem3  31990  noetalem5  31992  conway  32035  ifscgr  32276  cgrxfr  32287  outsideofeu  32363  linethru  32385  neibastop1  32479  dnicn  32607  fin2so  33526  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem28  33567  poimirlem31  33570  mblfinlem2  33577  mblfinlem3  33578  itg2addnclem  33591  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ssbnd  33717  totbndbnd  33718  prtlem10  34469  lssats  34617  lkrlss  34700  lshpset2N  34724  2dim  35074  islvol5  35183  paddasslem11  35434  pexmidlem8N  35581  ltrnid  35739  idltrn  35754  trlator0  35776  trlnidatb  35782  cdlemf2  36167  cdlemg2cex  36196  tendodi1  36389  tendodi2  36390  diblss  36776  dihopelvalcpre  36854  dih1dimatlem  36935  dihglblem6  36946  mzpsubst  37628  mzpcompact2lem  37631  eldioph2  37642  eldioph2b  37643  diophren  37694  pell14qrexpcl  37748  elpell1qr2  37753  monotoddzzfi  37824  acongtr  37862  acongrep  37864  jm2.19lem4  37876  jm2.26a  37884  jm2.26lem3  37885  jm2.26  37886  isnumbasgrplem2  37991  mendassa  38081  clsk3nimkb  38655  prmunb2  38827  4an4132  39022  fiiuncl  39548  ssinc  39578  ssdec  39579  supxrgelem  39866  infxr  39896  mullimc  40166  mullimcf  40173  neglimc  40197  climleltrp  40226  climisp  40296  limsupresxr  40316  liminfresxr  40317  liminflimsupclim  40357  icccncfext  40418  cncfiooicclem1  40424  fprodcncf  40432  dvnprodlem3  40481  iblcncfioo  40512  itgspltprt  40513  stoweidlem7  40542  stoweidlem28  40563  stoweidlem34  40569  stoweidlem48  40583  stoweidlem52  40587  wallispilem3  40602  fourierdlem12  40654  fourierdlem38  40680  fourierdlem39  40681  fourierdlem42  40684  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem65  40706  fourierdlem73  40714  fourierdlem76  40717  fourierdlem87  40728  fourierdlem103  40744  fourierdlem104  40745  sge0f1o  40917  sge0le  40942  sge0reuz  40982  ismeannd  41002  isomenndlem  41065  hoicvr  41083  hoidmvle  41135  smflimlem2  41301  smflimmpt  41337  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  mgmhmeql  42128
  Copyright terms: Public domain W3C validator