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

Theorem simpll2 1209
 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 1133 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antrr 724 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083 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 209  df-an 399  df-3an 1085 This theorem is referenced by:  f1prex  7034  wemappo  9007  iunfictbso  9534  fin1a2lem13  9828  prlem934  10449  ifle  12584  ixxlb  12754  elfzonelfzo  13133  swrdcl  14001  subcn2  14945  qexpz  16231  mreexexd  16913  initoeu2lem2  17269  issubmnd  17932  gsumccatOLD  17999  frmdup3lem  18025  pmtrf  18577  pgpssslw  18733  lsmmod  18795  reslmhm2b  19820  lsmcl  19849  lbsextlem3  19926  coe1mul2  20431  coe1fzgsumdlem  20463  evl1gsumdlem  20513  frlmsslsp  20934  islindf4  20976  scmate  21113  mdetdiaglem  21201  madurid  21247  cramerlem2  21291  pmatcollpw3lem  21385  iscnp4  21865  cnrest2  21888  ordthauslem  21985  cncmp  21994  clsconn  22032  rnelfmlem  22554  flimrest  22585  isfcf  22636  cnpfcf  22643  alexsubALT  22653  cldsubg  22713  utop2nei  22853  neipcfilu  22899  blssps  23028  blss  23029  stdbdbl  23121  metcnp3  23144  nmoeq0  23339  xrsxmet  23411  metdseq0  23456  addcnlem  23466  xrhmeo  23544  nmhmcn  23718  cfilres  23893  lgsfcl2  25873  lgsdir  25902  lgsne0  25905  istrkgcb  26236  axcontlem2  26745  axcontlem7  26750  axcontlem8  26751  subupgr  27063  clwwlknonex2  27882  frgr3v  28048  pjhthmo  29073  xrge0adddir  30674  dimvalfi  30997  pcmplfinf  31120  probun  31672  satfv1lem  32604  frpomin  33073  fprlem2  33133  nosupbnd1lem3  33205  nosupbnd1lem4  33206  nosupbnd1lem5  33207  nosupbnd2  33211  trisegint  33484  btwnconn1lem13  33555  outsideoftr  33585  outsideofeq  33586  linethru  33609  isbasisrelowllem1  34630  atlatmstc  36449  cvlcvr1  36469  hlrelat  36532  intnatN  36537  cvrval5  36545  2at0mat0  36655  llncvrlpln  36688  lplnexllnN  36694  lplncvrlvol  36746  lncvrelatN  36911  lncmp  36913  paddasslem5  36954  pmapjoin  36982  pmapjat1  36983  pclclN  37021  lhprelat3N  37170  cdleme32fvcl  37570  cdlemg1a  37700  cdlemg1cN  37717  cdlemg39  37846  ltrncom  37868  dihmeetALTN  38457  dihlspsnat  38463  mapdrvallem2  38775  mzpsubst  39338  lzunuz  39358  acongeq  39573  jm2.19  39583  jm2.27  39598  aomclem6  39652  lmhmfgsplit  39679  hbtlem5  39721  iunrelexpuztr  40057  ismnu  40590  3adantll3  41294  ioondisj2  41759  ioondisj1  41760  iccintsng  41791  icccncfext  42162  stoweidlem61  42339  fourierdlem42  42427  fourierdlem73  42457  smflimlem2  43041  domnmsuppn0  44410  lincresunit3  44529  nnolog2flm1  44643  itschlc0xyqsol1  44746  itschlc0xyqsol  44747
 Copyright terms: Public domain W3C validator