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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1062 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 481 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  f1prex  6524  ordiso2  8405  hartogslem1  8432  wemappo  8439  wemapso2lem  8442  acndom  8859  fin1a2lem12  9218  fin1a2lem13  9219  prlem934  9840  ifle  12013  lcmfunsnlem2lem1  15332  divgcdcoprm0  15360  rpexp  15413  qexpz  15586  ramval  15693  0ram  15705  ramz2  15709  initoeu2lem2  16646  mrelatglb  17165  dfgrp3lem  17494  odbezout  17956  lsmcl  19064  lbsextlem3  19141  psropprmul  19589  coe1mul2  19620  coe1fzgsumdlem  19652  evl1gsumdlem  19701  frlmsslsp  20116  islindf4  20158  scmate  20297  mdetunilem7  20405  mdetmul  20410  cramerlem2  20475  m2pmfzgsumcl  20534  decpmatmul  20558  pmatcollpw3lem  20569  chpdmatlem2  20625  cpmadugsumlemB  20660  cpmadugsumlemC  20661  cpmadugsumlemF  20662  chcoeffeqlem  20671  cnconst2  21068  ordthauslem  21168  clsconn  21214  restnlly  21266  comppfsc  21316  ptpjopn  21396  trfg  21676  rnelfmlem  21737  isfcf  21819  fcfnei  21820  cnpfcf  21826  utop2nei  22035  neipcfilu  22081  blssps  22210  blss  22211  metcnp  22327  xrsxmet  22593  metdsge  22633  metdseq0  22638  addcnlem  22648  xrhmeo  22726  nmhmcn  22901  caucfil  23062  limcfval  23617  fta1b  23910  lgsmod  25029  lgsdir  25038  lgsne0  25041  axpasch  25802  axcontlem2  25826  wpthswwlks2on  26835  clwwlksnwwlkncl  26901  frgr3v  27119  pjhthmo  28131  difioo  29518  xrge0adddir  29666  archiabl  29726  rhmdvdsr  29792  probun  30455  nosupbnd1lem3  31830  nosupbnd1lem4  31831  nosupbnd1lem5  31832  nosupbnd2  31836  scutun12  31891  trisegint  32110  btwnconn1lem13  32181  brsegle2  32191  linethru  32235  hlrelat  34507  intnatN  34512  lnnat  34532  3dim0  34562  3dim1  34572  3dim2  34573  atcvrlln  34625  llnexatN  34626  2at0mat0  34630  llncvrlpln  34663  lplnexllnN  34669  lplncvrlvol  34721  lncvrelatN  34886  lncmp  34888  elpaddn0  34905  paddasslem5  34929  pmapjoin  34957  pmapjat1  34958  pclclN  34996  osumclN  35072  lhprelat3N  35145  trlval4  35294  cdlemd5  35308  cdleme32fvcl  35547  cdleme42keg  35593  cdlemg1a  35677  cdlemg1cN  35694  cdlemg39  35823  ltrncom  35845  cdlemk34  36017  dihord2pre  36333  dihopelvalcpre  36356  dihmeetALTN  36435  dihlspsnssN  36440  dihlspsnat  36441  diophrw  37141  lzunuz  37150  qirropth  37292  jm2.19  37379  jm2.27  37394  lmhmfgsplit  37475  hbtlem5  37517  iunrelexpuztr  37830  rfcnnnub  39015  3adantll2  39022  3adantll3  39023  ioondisj2  39517  ioondisj1  39518  iccintsng  39552  icccncfext  39863  stoweidlem20  40000  stoweidlem61  40041  smflimlem2  40743  rmsupp0  41914  rmsuppss  41916  ply1mulgsum  41943
  Copyright terms: Public domain W3C validator