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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simp2 1167 . 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  6735  wemappo  8665  iunfictbso  9192  fin1a2lem13  9491  prlem934  10112  ifle  12237  ixxlb  12406  elfzonelfzo  12785  swrdcl  13629  subcn2  14626  qexpz  15900  mreexexd  16590  initoeu2lem2  16946  issubmnd  17600  gsumccat  17660  frmdup3lem  17686  pmtrf  18154  pgpssslw  18309  lsmmod  18368  reslmhm2b  19342  lsmcl  19371  lbsextlem3  19450  coe1mul2  19928  coe1fzgsumdlem  19960  evl1gsumdlem  20009  frlmsslsp  20427  islindf4  20469  scmate  20609  mdetdiaglem  20697  madurid  20743  cramerlem2  20789  pmatcollpw3lem  20883  iscnp4  21363  cnrest2  21386  ordthauslem  21483  cncmp  21491  clsconn  21529  rnelfmlem  22051  flimrest  22082  isfcf  22133  cnpfcf  22140  alexsubALT  22150  cldsubg  22209  utop2nei  22349  neipcfilu  22395  blssps  22524  blss  22525  stdbdbl  22617  metcnp3  22640  nmoeq0  22835  xrsxmet  22907  metdseq0  22952  addcnlem  22962  xrhmeo  23040  nmhmcn  23214  cfilres  23389  lgsfcl2  25335  lgsdir  25364  lgsne0  25367  istrkgcb  25662  axcontlem2  26152  axcontlem7  26157  axcontlem8  26158  subupgr  26474  wpthswwlks2onOLD  27206  clwwlknonex2  27403  frgr3v  27578  pjhthmo  28640  xrge0adddir  30162  pcmplfinf  30398  probun  30952  frpomin  32205  nosupbnd1lem3  32323  nosupbnd1lem4  32324  nosupbnd1lem5  32325  nosupbnd2  32329  trisegint  32602  btwnconn1lem13  32673  outsideoftr  32703  outsideofeq  32704  linethru  32727  isbasisrelowllem1  33659  atlatmstc  35298  cvlcvr1  35318  hlrelat  35381  intnatN  35386  cvrval5  35394  2at0mat0  35504  llncvrlpln  35537  lplnexllnN  35543  lplncvrlvol  35595  lncvrelatN  35760  lncmp  35762  paddasslem5  35803  pmapjoin  35831  pmapjat1  35832  pclclN  35870  lhprelat3N  36019  cdleme32fvcl  36419  cdlemg1a  36549  cdlemg1cN  36566  cdlemg39  36695  ltrncom  36717  dihmeetALTN  37306  dihlspsnat  37312  mapdrvallem2  37624  mzpsubst  38015  lzunuz  38035  acongeq  38253  jm2.19  38263  jm2.27  38278  aomclem6  38332  lmhmfgsplit  38359  hbtlem5  38401  iunrelexpuztr  38712  3adantll3  39881  ioondisj2  40382  ioondisj1  40383  iccintsng  40414  icccncfext  40764  stoweidlem61  40941  fourierdlem42  41029  fourierdlem73  41059  smflimlem2  41646  domnmsuppn0  42845  lincresunit3  42965  nnolog2flm1  43079
  Copyright terms: Public domain W3C validator