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

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

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1084 . 2 (((𝜑𝜓𝜒) ∧ 𝜃) → 𝜑)
21adantr 480 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  f1prex  6579  ordiso2  8461  hartogslem1  8488  wemappo  8495  wemapso2lem  8498  acndom  8912  fin1a2lem12  9271  fin1a2lem13  9272  prlem934  9893  ifle  12066  lcmfunsnlem2lem1  15398  divgcdcoprm0  15426  rpexp  15479  qexpz  15652  ramval  15759  0ram  15771  ramz2  15775  initoeu2lem2  16712  mrelatglb  17231  dfgrp3lem  17560  odbezout  18021  lsmcl  19131  lbsextlem3  19208  psropprmul  19656  coe1mul2  19687  coe1fzgsumdlem  19719  evl1gsumdlem  19768  frlmsslsp  20183  islindf4  20225  scmate  20364  mdetunilem7  20472  mdetmul  20477  cramerlem2  20542  m2pmfzgsumcl  20601  decpmatmul  20625  pmatcollpw3lem  20636  chpdmatlem2  20692  cpmadugsumlemB  20727  cpmadugsumlemC  20728  cpmadugsumlemF  20729  chcoeffeqlem  20738  cnconst2  21135  ordthauslem  21235  clsconn  21281  restnlly  21333  comppfsc  21383  ptpjopn  21463  trfg  21742  rnelfmlem  21803  isfcf  21885  fcfnei  21886  cnpfcf  21892  utop2nei  22101  neipcfilu  22147  blssps  22276  blss  22277  metcnp  22393  xrsxmet  22659  metdsge  22699  metdseq0  22704  addcnlem  22714  xrhmeo  22792  nmhmcn  22966  caucfil  23127  limcfval  23681  fta1b  23974  lgsmod  25093  lgsdir  25102  lgsne0  25105  axpasch  25866  axcontlem2  25890  wpthswwlks2onOLD  26928  clwwlknonex2  27084  frgr3v  27255  pjhthmo  28289  difioo  29672  xrge0adddir  29820  archiabl  29880  rhmdvdsr  29946  probun  30609  nosupbnd1lem3  31981  nosupbnd1lem4  31982  nosupbnd1lem5  31983  nosupbnd2  31987  scutun12  32042  trisegint  32260  btwnconn1lem13  32331  brsegle2  32341  linethru  32385  hlrelat  35006  intnatN  35011  lnnat  35031  3dim0  35061  3dim1  35071  3dim2  35072  atcvrlln  35124  llnexatN  35125  2at0mat0  35129  llncvrlpln  35162  lplnexllnN  35168  lplncvrlvol  35220  lncvrelatN  35385  lncmp  35387  elpaddn0  35404  paddasslem5  35428  pmapjoin  35456  pmapjat1  35457  pclclN  35495  osumclN  35571  lhprelat3N  35644  trlval4  35793  cdlemd5  35807  cdleme32fvcl  36045  cdleme42keg  36091  cdlemg1a  36175  cdlemg1cN  36192  cdlemg39  36321  ltrncom  36343  cdlemk34  36515  dihord2pre  36831  dihopelvalcpre  36854  dihmeetALTN  36933  dihlspsnssN  36938  dihlspsnat  36939  diophrw  37639  lzunuz  37648  qirropth  37790  jm2.19  37877  jm2.27  37892  lmhmfgsplit  37973  hbtlem5  38015  iunrelexpuztr  38328  rfcnnnub  39509  3adantll2  39516  3adantll3  39517  ioondisj2  40032  ioondisj1  40033  iccintsng  40067  icccncfext  40418  stoweidlem20  40555  stoweidlem61  40596  smflimlem2  41301  rmsupp0  42474  rmsuppss  42476  ply1mulgsum  42503
  Copyright terms: Public domain W3C validator