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

Theorem simpll1 1092
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1056 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 479 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  f1prex  6414  ordiso2  8277  hartogslem1  8304  wemappo  8311  wemapso2lem  8314  acndom  8731  fin1a2lem12  9090  fin1a2lem13  9091  prlem934  9708  ifle  11858  lcmfunsnlem2lem1  15132  divgcdcoprm0  15160  rpexp  15213  qexpz  15386  ramval  15493  0ram  15505  ramz2  15509  initoeu2lem2  16431  mrelatglb  16950  dfgrp3lem  17279  odbezout  17741  lsmcl  18847  lbsextlem3  18924  psropprmul  19372  coe1mul2  19403  coe1fzgsumdlem  19435  evl1gsumdlem  19484  frlmsslsp  19893  islindf4  19935  scmate  20074  mdetunilem7  20182  mdetmul  20187  cramerlem2  20252  m2pmfzgsumcl  20311  decpmatmul  20335  pmatcollpw3lem  20346  chpdmatlem2  20402  cpmadugsumlemB  20437  cpmadugsumlemC  20438  cpmadugsumlemF  20439  chcoeffeqlem  20448  cnconst2  20836  ordthauslem  20936  clscon  20982  restnlly  21034  comppfsc  21084  ptpjopn  21164  trfg  21444  rnelfmlem  21505  isfcf  21587  fcfnei  21588  cnpfcf  21594  utop2nei  21803  neipcfilu  21849  blssps  21977  blss  21978  metcnp  22094  xrsxmet  22349  metdsge  22388  metdseq0  22393  addcnlem  22403  xrhmeo  22481  nmhmcn  22656  caucfil  22804  limcfval  23356  fta1b  23647  lgsmod  24762  lgsdir  24771  lgsne0  24774  axpasch  25536  axcontlem2  25560  clwwlknwwlkncl  26091  clwlkf1clwwlk  26140  pjhthmo  27348  difioo  28737  xrge0adddir  28826  archiabl  28886  rhmdvdsr  28952  probun  29611  trisegint  31108  btwnconn1lem13  31179  brsegle2  31189  linethru  31233  hlrelat  33506  intnatN  33511  lnnat  33531  3dim0  33561  3dim1  33571  3dim2  33572  atcvrlln  33624  llnexatN  33625  2at0mat0  33629  llncvrlpln  33662  lplnexllnN  33668  lplncvrlvol  33720  lncvrelatN  33885  lncmp  33887  elpaddn0  33904  paddasslem5  33928  pmapjoin  33956  pmapjat1  33957  pclclN  33995  osumclN  34071  lhprelat3N  34144  trlval4  34293  cdlemd5  34307  cdleme32fvcl  34546  cdleme42keg  34592  cdlemg1a  34676  cdlemg1cN  34693  cdlemg39  34822  ltrncom  34844  cdlemk34  35016  dihord2pre  35332  dihopelvalcpre  35355  dihmeetALTN  35434  dihlspsnssN  35439  dihlspsnat  35440  diophrw  36140  lzunuz  36149  qirropth  36291  jm2.19  36378  jm2.27  36393  lmhmfgsplit  36474  hbtlem5  36517  iunrelexpuztr  36830  rfcnnnub  38018  3adantll2  38025  3adantll3  38026  ioondisj2  38362  ioondisj1  38363  iccintsng  38397  icccncfext  38574  stoweidlem20  38714  stoweidlem61  38755  smflimlem2  39459  wpthswwlks2on  41163  clwwlksnwwlkncl  41227  frgr3v  41444  frgr2wwlkeqm  41495  rmsupp0  41942  rmsuppss  41944  ply1mulgsum  41971
  Copyright terms: Public domain W3C validator