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

Theorem simplll 773
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 728 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 206  df-an 397
This theorem is referenced by:  f1imass  7207  poseq  8082  oeeui  8541  oaabs2  8587  omxpenlem  8975  findcard3  9187  wemappo  9443  acndom2  9948  infpwfien  9956  sornom  10171  isf32lem2  10248  isf32lem4  10250  fin1a2lem11  10304  pwfseq  10558  gchina  10593  inttsk  10668  inar1  10669  prlem936  10941  mulcmpblnr  10965  00id  11288  mul02lem1  11289  addid1  11293  cnegex  11294  negeu  11349  add20  11625  ltmul12a  11969  lediv12a  12006  cru  12103  qextltlem  13075  xmullem  13137  xlemul1a  13161  ixxss12  13238  ioodisj  13353  elfz0fzfz0  13500  fsuppmapnn0fz  13855  seqf1o  13903  mulexpz  13962  leexp1a  14034  seqcoll  14317  swrdswrdlem  14550  pfxccatin12lem3  14578  abs3lem  15183  cau3lem  15199  climcau  15515  sumeq2ii  15538  climcndslem1  15694  climcndslem2  15695  geomulcvg  15721  mertenslem1  15729  mertenslem2  15730  mertens  15731  prodeq2ii  15756  prodmolem2  15778  bitsfzo  16275  sadadd2lem2  16290  dvdsmulgcd  16396  qredeu  16494  pc2dvds  16711  pcz  16713  ramcl  16861  firest  17274  mreexexlemd  17484  isacs2  17493  iscatd2  17521  ipodrsima  18390  mrelatlub  18411  mndpropd  18541  mhmeql  18596  mhmid  18827  mhmmnd  18828  issubg4  18906  cycsubm  18954  cycsubmcom  18956  gasubg  19041  symgextf  19158  pmtr3ncom  19216  gexdvds  19325  oddvdssubg  19592  cyggeninv  19619  cyggenod  19620  issrg  19878  dvdsrmul1  20035  unitgrp  20049  cntzsubr  20208  islmhm2  20452  lmhmeql  20469  lbspropd  20513  lssacsex  20558  psgndiflemA  20958  isphl  20985  ocvocv  21028  lindfmm  21186  issubassa2  21248  mplbas2  21395  scmatmats  21812  smatvscl  21825  mdetdiag  21900  m2cpmfo  22057  pmatcollpw3fi1lem1  22087  pm2mpf1  22100  pm2mpghm  22117  fvmptnn04if  22150  chfacfscmulfsupp  22160  chfacfpmmulfsupp  22164  neissex  22430  neiptoptop  22434  neiptopnei  22435  restbas  22461  tgrest  22462  restopnb  22478  cnpco  22570  isreg2  22680  iunconn  22731  1stcrest  22756  2ndcctbss  22758  2ndcomap  22761  2ndcsep  22762  dislly  22800  kgencn2  22860  ptbasfi  22884  txhaus  22950  txkgen  22955  txconn  22992  qtopcn  23017  regr1lem2  23043  kqnrmlem1  23046  kqnrmlem2  23047  trfbas2  23146  trfil2  23190  flimcf  23285  hauspwpwf1  23290  fclscf  23328  flimfnfcls  23331  ustexsym  23519  ustuqtop4  23548  utop3cls  23555  utopreg  23556  ucnima  23585  ucncn  23589  metequiv2  23818  prdsxmslem2  23837  metcnpi3  23854  metustto  23861  metustid  23862  metustexhalf  23864  ngptgp  23944  xrsblre  24126  icccmp  24140  reconnlem1  24141  reconn  24143  opnreen  24146  metdsf  24163  metdscn  24171  fsumcn  24185  elcncf2  24205  cncfmet  24224  pcoass  24339  lmcau  24629  rrxdstprj1  24725  pmltpc  24766  ivthlem2  24768  ivthlem3  24769  ovollb2  24805  volsup  24872  ioombl1  24878  ioorf  24889  dyadss  24910  dyaddisjlem  24911  dyadmax  24914  volcn  24922  cncombf  24974  mbflimsup  24982  itg2const2  25058  iblss2  25122  cpnord  25251  dvmptfsum  25291  fta1g  25484  plydivex  25609  fta1  25620  aannenlem1  25640  ulmdvlem3  25713  advlogexp  25962  cxpmul2z  25998  atantayl2  26240  jensen  26290  isppw2  26416  lgsqr  26651  lgsqrmodndvds  26653  lgsdchrval  26654  lgsquad3  26687  2sqb  26732  dchrisumlem3  26791  pntrsumbnd2  26867  noinfbnd1lem5  27027  noetasuplem4  27036  noetainflem4  27040  noetalem1  27041  conway  27090  madebdayim  27168  madebdaylemlrcut  27177  tgjustf  27244  axsegcon  27705  axeuclidlem  27740  axcontlem9  27750  eengtrkg  27764  cusgrsize2inds  28230  pthdepisspth  28512  usgr2wlkneq  28533  crctcshwlkn0  28595  wpthswwlks2on  28735  clwwlkccatlem  28762  wwlksext2clwwlk  28830  umgr3v3e3cycl  28957  vdgn1frgrv2  29069  frgrwopreglem5  29094  frgrwopreg  29096  frgrhash2wsp  29105  numclwwlk1lem2fo  29131  vacn  29465  smcnlem  29468  0lno  29561  chocunii  30072  occl  30075  5oalem1  30425  3oalem2  30434  unoplin  30691  hmoplin  30713  lnconi  30804  kbass5  30891  mdslmd1lem1  31096  mdslmd1lem2  31097  mdsymlem2  31175  cdj1i  31204  opreu2reuALT  31234  unidifsnne  31292  disjabrex  31329  disjabrexf  31330  acunirnmpt  31404  fgreu  31417  suppovss  31425  xrge0infss  31491  xrofsup  31498  fsumiunle  31551  mgcf1o  31689  xrge0addgt0  31708  submomnd  31744  fzto1st1  31777  cyc3genpm  31827  cycpmgcl  31828  submarchi  31848  archiabllem1  31855  archiabllem2a  31856  isarchiofld  31938  imaslmod  31971  lindfpropd  31995  elrspunidl  32025  lvecdim0  32124  locfinreflem  32233  zarcmplem  32274  rge0scvg  32342  lmxrge0  32345  lmdvg  32346  qqhval2  32375  esumrnmpt2  32479  esumfsup  32481  esumpcvgval  32489  esumcvg  32497  esumgect  32501  esumiun  32505  sigaclfu2  32532  sigainb  32547  insiga  32548  fiunelros  32585  measinblem  32631  measinb  32632  measdivcst  32635  measdivcstALTV  32636  omssubadd  32712  oddpwdc  32766  dstrvprob  32883  sgnmul  32954  sgnsub  32956  signsply0  32975  signstfvneq0  32996  bnj1408  33460  ptpconn  33639  sconnpi1  33645  resconn  33652  cvmliftmolem2  33688  cvmlift2lem12  33720  satfsschain  33770  satffunlem2lem1  33810  naddssim  34240  negsprop  34328  ifscgr  34567  cgrxfr  34578  outsideofeu  34654  linethru  34676  neibastop1  34769  dnicn  34893  irrdifflemf  35734  irrdiff  35735  fin2so  36003  matunitlindflem1  36012  matunitlindflem2  36013  poimirlem28  36044  poimirlem31  36047  mblfinlem2  36054  mblfinlem3  36055  itg2addnclem  36067  ftc1anclem7  36095  ftc1anclem8  36096  ftc1anc  36097  ssbnd  36185  totbndbnd  36186  prtlem10  37265  lssats  37412  lkrlss  37495  lshpset2N  37519  2dim  37871  islvol5  37980  paddasslem11  38231  pexmidlem8N  38378  ltrnid  38536  idltrn  38551  trlator0  38572  trlnidatb  38578  cdlemf2  38963  cdlemg2cex  38992  tendodi1  39185  tendodi2  39186  diblss  39571  dihopelvalcpre  39649  dih1dimatlem  39730  dihglblem6  39741  sticksstones22  40514  remul01  40785  sn-subeu  40804  sn-0tie0  40817  itrere  40844  retire  40845  prjspertr  40852  prjspersym  40854  0prjspnrel  40874  mzpsubst  40980  mzpcompact2lem  40983  eldioph2  40994  eldioph2b  40995  diophren  41045  pell14qrexpcl  41099  elpell1qr2  41104  monotoddzzfi  41175  acongtr  41211  acongrep  41213  jm2.19lem4  41225  jm2.26a  41233  jm2.26lem3  41234  jm2.26  41235  isnumbasgrplem2  41340  mendassa  41430  omord2lim  41542  cantnftermord  41562  naddcnffo  41585  naddcnfcom  41587  naddcnfid1  41588  clsk3nimkb  42223  prmunb2  42502  4an4132  42692  fiiuncl  43184  ssinc  43208  ssdec  43209  supxrgelem  43476  infxr  43506  mullimc  43758  mullimcf  43765  neglimc  43789  climleltrp  43818  climisp  43888  limsupresxr  43908  liminfresxr  43909  liminflimsupclim  43949  xlimliminflimsup  44004  icccncfext  44029  cncfiooicclem1  44035  fprodcncf  44042  dvnprodlem3  44090  iblcncfioo  44120  itgspltprt  44121  stoweidlem7  44149  stoweidlem28  44170  stoweidlem34  44176  stoweidlem48  44190  stoweidlem52  44194  wallispilem3  44209  fourierdlem12  44261  fourierdlem38  44287  fourierdlem39  44288  fourierdlem42  44291  fourierdlem46  44294  fourierdlem48  44296  fourierdlem49  44297  fourierdlem50  44298  fourierdlem51  44299  fourierdlem65  44313  fourierdlem73  44321  fourierdlem76  44324  fourierdlem87  44335  fourierdlem103  44351  fourierdlem104  44352  sge0f1o  44524  sge0le  44549  sge0reuz  44589  ismeannd  44609  isomenndlem  44672  hoicvr  44690  hoidmvle  44742  smflimlem2  44914  smflimmpt  44952  fsupdm  44984  finfdm  44988  imasetpreimafvbijlemf1  45497  nnsum4primeseven  45893  nnsum4primesevenALTV  45894  bgoldbtbndlem2  45899  bgoldbtbndlem3  45900  bgoldbtbnd  45902  isomuspgrlem2  45926  mgmhmeql  45998  rrxlinec  46723  iccdisj  46832  fullthinc  46967
  Copyright terms: Public domain W3C validator