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

Theorem simpll3 1259
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 1133 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antrr 764 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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  df-3an 1074
This theorem is referenced by:  f1prex  6702  ordiso2  8585  wemappo  8619  iunfictbso  9127  fin1a2lem12  9425  fin1a2lem13  9426  prlem934  10047  ifle  12221  xlesubadd  12286  icoshftf1o  12488  elfzonelfzo  12764  fsuppmapnn0fiub0  12987  swrdcl  13618  repswccat  13732  subcn2  14524  rpdvds  15576  coprmprod  15577  qexpz  15807  ramval  15914  0ram  15926  cshwrepswhash1  16011  mreexexd  16510  gsumccat  17579  gsmsymgreqlem1  18050  pmtrf  18075  odmulg  18173  pgpfi1  18210  lsmcl  19285  lbsextlem3  19362  coe1mul2  19841  islindf4  20379  cramerlem2  20696  cpmadugsumlemF  20883  cayhamlem4  20895  iscnp4  21269  cnpnei  21270  cnconst2  21289  cnpdis  21299  cnhaus  21360  ordthauslem  21389  clsconn  21435  nlly2i  21481  txcn  21631  ordthmeolem  21806  flimrest  21988  isfcf  22039  alexsubALTlem4  22055  ghmcnp  22119  utop2nei  22255  blssps  22430  blss  22431  metcnp3  22546  metcnp  22547  xrsxmet  22813  metdseq0  22858  xrhmeo  22946  cfil3i  23267  caucfil  23281  cfilres  23294  fta1b  24128  mumul  25106  lgsfcl2  25227  lgsdir  25256  lgsne0  25259  istrkgcb  25554  axbtwnid  26018  axcontlem2  26044  axcontlem4  26046  axcontlem7  26049  axcontlem8  26050  umgr2v2enb1  26632  wpthswwlks2onOLD  27083  frgr3v  27429  extwwlkfab  27511  pjhthmo  28470  xrge0adddir  30001  archiabl  30061  pcmplfinf  30237  probun  30790  cnpconn  31519  nolt02o  32151  nosupbnd1lem3  32162  nosupbnd1lem4  32163  nosupbnd1lem5  32164  nosupbnd2  32168  outsideofeq  32543  linethru  32566  atlatmstc  35109  cvlcvr1  35129  ishlat3N  35144  hlrelat  35191  intnatN  35196  cvrval5  35204  atcvrlln  35309  llnexatN  35310  2at0mat0  35314  llncvrlpln  35347  lplnexllnN  35353  lplncvrlvol  35405  lncvrelatN  35570  pmapjoin  35641  pmapjat1  35642  pclclN  35680  osumclN  35756  lhprelat3N  35829  cdlemd5  35992  cdleme32fvcl  36230  cdlemg39  36506  ltrncom  36528  dihmeetALTN  37118  dochss  37156  mapdrvallem2  37436  nacsfix  37777  mzpsubst  37813  diophrw  37824  lzunuz  37833  jm2.19  38062  jm2.27  38077  hbtlem5  38200  iunrelexpuztr  38513  rfcnnnub  39694  3adantll2  39701  infleinf  40086  iccintsng  40252  mullimc  40351  mullimcf  40358  limcperiod  40363  cncfshift  40590  cncfperiod  40595  icccncfext  40603  stoweidlem20  40740  stoweidlem61  40781  fourierdlem73  40899  rmsupp0  42659  rmsuppss  42661
  Copyright terms: Public domain W3C validator