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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simp1 1128 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antrr 722 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  f1prex  7031  ordiso2  8967  hartogslem1  8994  wemappo  9001  wemapso2lem  9004  acndom  9465  fin1a2lem12  9821  fin1a2lem13  9822  prlem934  10443  ifle  12578  lcmfunsnlem2lem1  15970  divgcdcoprm0  15997  rpexp  16052  qexpz  16225  ramval  16332  0ram  16344  ramz2  16348  initoeu2lem2  17263  mrelatglb  17782  dfgrp3lem  18135  odbezout  18614  lsmcl  19784  lbsextlem3  19861  psropprmul  20334  coe1mul2  20365  coe1fzgsumdlem  20397  evl1gsumdlem  20447  frlmsslsp  20868  islindf4  20910  scmate  21047  mdetunilem7  21155  mdetmul  21160  cramerlem2  21225  m2pmfzgsumcl  21284  decpmatmul  21308  pmatcollpw3lem  21319  chpdmatlem2  21375  cpmadugsumlemB  21410  cpmadugsumlemC  21411  cpmadugsumlemF  21412  chcoeffeqlem  21421  cnconst2  21819  ordthauslem  21919  clsconn  21966  restnlly  22018  comppfsc  22068  ptpjopn  22148  trfg  22427  rnelfmlem  22488  isfcf  22570  fcfnei  22571  cnpfcf  22577  utop2nei  22786  neipcfilu  22832  blssps  22961  blss  22962  metcnp  23078  xrsxmet  23344  metdsge  23384  metdseq0  23389  addcnlem  23399  xrhmeo  23477  nmhmcn  23651  caucfil  23813  limcfval  24397  fta1b  24690  lgsmod  25826  lgsdir  25835  lgsne0  25838  axpasch  26654  axcontlem2  26678  clwwlknonex2  27815  frgr3v  27981  pjhthmo  29006  difioo  30431  xrge0adddir  30606  archiabl  30754  rhmdvdsr  30818  dimvalfi  30901  probun  31576  satfv1lem  32506  nosupbnd1lem3  33107  nosupbnd1lem4  33108  nosupbnd1lem5  33109  nosupbnd2  33113  scutun12  33168  trisegint  33386  btwnconn1lem13  33457  brsegle2  33467  linethru  33511  lindsadd  34766  hlrelat  36418  intnatN  36423  lnnat  36443  3dim0  36473  3dim1  36483  3dim2  36484  atcvrlln  36536  llnexatN  36537  2at0mat0  36541  llncvrlpln  36574  lplnexllnN  36580  lplncvrlvol  36632  lncvrelatN  36797  lncmp  36799  elpaddn0  36816  paddasslem5  36840  pmapjoin  36868  pmapjat1  36869  pclclN  36907  osumclN  36983  lhprelat3N  37056  trlval4  37204  cdlemd5  37218  cdleme32fvcl  37456  cdleme42keg  37502  cdlemg1a  37586  cdlemg1cN  37603  cdlemg39  37732  ltrncom  37754  cdlemk34  37926  dihord2pre  38241  dihopelvalcpre  38264  dihmeetALTN  38343  dihlspsnssN  38348  dihlspsnat  38349  diophrw  39234  lzunuz  39243  qirropth  39383  jm2.19  39468  jm2.27  39483  lmhmfgsplit  39564  hbtlem5  39606  iunrelexpuztr  39942  rfcnnnub  41170  3adantll2  41177  3adantll3  41178  ioondisj2  41643  ioondisj1  41644  iccintsng  41675  icccncfext  42046  stoweidlem20  42182  stoweidlem61  42223  smflimlem2  42925  rmsupp0  44344  rmsuppss  44346  ply1mulgsum  44372  rrxlinesc  44650
  Copyright terms: Public domain W3C validator