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

Theorem simpll3 1273
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simpll3 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)

Proof of Theorem simpll3
StepHypRef Expression
1 simp3 1168 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antrr 717 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1107
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 198  df-an 385  df-3an 1109
This theorem is referenced by:  f1prex  6731  ordiso2  8627  wemappo  8661  iunfictbso  9188  fin1a2lem12  9486  fin1a2lem13  9487  prlem934  10108  ifle  12230  xlesubadd  12295  icoshftf1o  12500  elfzonelfzo  12778  fsuppmapnn0fiub0  13000  swrdcl  13620  repswccat  13810  subcn2  14610  rpdvds  15654  coprmprod  15655  qexpz  15884  ramval  15991  0ram  16003  cshwrepswhash1  16083  mreexexd  16574  gsumccat  17644  gsmsymgreqlem1  18113  pmtrf  18138  odmulg  18237  pgpfi1  18274  lsmcl  19355  lbsextlem3  19434  coe1mul2  19912  islindf4  20453  cramerlem2  20773  cpmadugsumlemF  20960  cayhamlem4  20972  iscnp4  21347  cnpnei  21348  cnconst2  21367  cnpdis  21377  cnhaus  21438  ordthauslem  21467  clsconn  21513  nlly2i  21559  txcn  21709  ordthmeolem  21884  flimrest  22066  isfcf  22117  alexsubALTlem4  22133  ghmcnp  22197  utop2nei  22333  blssps  22508  blss  22509  metcnp3  22624  metcnp  22625  xrsxmet  22891  metdseq0  22936  xrhmeo  23024  cfil3i  23346  caucfil  23360  cfilres  23373  fta1b  24220  mumul  25198  lgsfcl2  25319  lgsdir  25348  lgsne0  25351  istrkgcb  25646  axbtwnid  26110  axcontlem2  26136  axcontlem4  26138  axcontlem7  26141  axcontlem8  26142  umgr2v2enb1  26713  wpthswwlks2onOLD  27186  frgr3v  27555  extwwlkfab  27641  extwwlkfabOLD  27642  pjhthmo  28617  xrge0adddir  30139  archiabl  30199  pcmplfinf  30375  probun  30929  cnpconn  31660  nolt02o  32289  nosupbnd1lem3  32300  nosupbnd1lem4  32301  nosupbnd1lem5  32302  nosupbnd2  32306  outsideofeq  32681  linethru  32704  atlatmstc  35275  cvlcvr1  35295  ishlat3N  35310  hlrelat  35358  intnatN  35363  cvrval5  35371  atcvrlln  35476  llnexatN  35477  2at0mat0  35481  llncvrlpln  35514  lplnexllnN  35520  lplncvrlvol  35572  lncvrelatN  35737  pmapjoin  35808  pmapjat1  35809  pclclN  35847  osumclN  35923  lhprelat3N  35996  cdlemd5  36158  cdleme32fvcl  36396  cdlemg39  36672  ltrncom  36694  dihmeetALTN  37283  dochss  37321  mapdrvallem2  37601  nacsfix  37953  mzpsubst  37989  diophrw  38000  lzunuz  38009  jm2.19  38237  jm2.27  38252  hbtlem5  38375  iunrelexpuztr  38686  rfcnnnub  39847  3adantll2  39854  infleinf  40226  iccintsng  40388  mullimc  40486  mullimcf  40493  limcperiod  40498  cncfshift  40725  cncfperiod  40730  icccncfext  40738  stoweidlem20  40874  stoweidlem61  40915  fourierdlem73  41033  rmsupp0  42818  rmsuppss  42820
  Copyright terms: Public domain W3C validator