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

Theorem simpll1 1209
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 1133 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antrr 725 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084
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 210  df-an 400  df-3an 1086
This theorem is referenced by:  f1prex  7014  ordiso2  8955  hartogslem1  8982  wemappo  8989  wemapso2lem  8992  acndom  9454  fin1a2lem12  9810  fin1a2lem13  9811  prlem934  10432  ifle  12568  lcmfunsnlem2lem1  15959  divgcdcoprm0  15986  rpexp  16041  qexpz  16214  ramval  16321  0ram  16333  ramz2  16337  initoeu2lem2  17253  mrelatglb  17772  dfgrp3lem  18175  odbezout  18663  lsmcl  19830  lbsextlem3  19907  psropprmul  20381  coe1mul2  20412  coe1fzgsumdlem  20444  evl1gsumdlem  20494  frlmsslsp  20915  islindf4  20957  scmate  21094  mdetunilem7  21202  mdetmul  21207  cramerlem2  21272  m2pmfzgsumcl  21331  decpmatmul  21355  pmatcollpw3lem  21366  chpdmatlem2  21422  cpmadugsumlemB  21457  cpmadugsumlemC  21458  cpmadugsumlemF  21459  chcoeffeqlem  21468  cnconst2  21866  ordthauslem  21966  clsconn  22013  restnlly  22065  comppfsc  22115  ptpjopn  22195  trfg  22474  rnelfmlem  22535  isfcf  22617  fcfnei  22618  cnpfcf  22624  utop2nei  22834  neipcfilu  22880  blssps  23009  blss  23010  metcnp  23126  xrsxmet  23392  metdsge  23432  metdseq0  23437  addcnlem  23447  xrhmeo  23529  nmhmcn  23703  caucfil  23865  limcfval  24453  fta1b  24748  lgsmod  25885  lgsdir  25894  lgsne0  25897  axpasch  26713  axcontlem2  26737  clwwlknonex2  27872  frgr3v  28038  pjhthmo  29063  difioo  30491  xrge0adddir  30686  archiabl  30834  rhmdvdsr  30898  ssmxidl  30989  dimvalfi  31012  probun  31684  satfv1lem  32616  nosupbnd1lem3  33217  nosupbnd1lem4  33218  nosupbnd1lem5  33219  nosupbnd2  33223  scutun12  33278  trisegint  33496  btwnconn1lem13  33567  brsegle2  33577  linethru  33621  lindsadd  34928  hlrelat  36576  intnatN  36581  lnnat  36601  3dim0  36631  3dim1  36641  3dim2  36642  atcvrlln  36694  llnexatN  36695  2at0mat0  36699  llncvrlpln  36732  lplnexllnN  36738  lplncvrlvol  36790  lncvrelatN  36955  lncmp  36957  elpaddn0  36974  paddasslem5  36998  pmapjoin  37026  pmapjat1  37027  pclclN  37065  osumclN  37141  lhprelat3N  37214  trlval4  37362  cdlemd5  37376  cdleme32fvcl  37614  cdleme42keg  37660  cdlemg1a  37744  cdlemg1cN  37761  cdlemg39  37890  ltrncom  37912  cdlemk34  38084  dihord2pre  38399  dihopelvalcpre  38422  dihmeetALTN  38501  dihlspsnssN  38506  dihlspsnat  38507  diophrw  39495  lzunuz  39504  qirropth  39644  jm2.19  39729  jm2.27  39744  lmhmfgsplit  39825  hbtlem5  39867  iunrelexpuztr  40199  rfcnnnub  41448  3adantll2  41455  3adantll3  41456  ioondisj2  41921  ioondisj1  41922  iccintsng  41951  icccncfext  42320  stoweidlem20  42453  stoweidlem61  42494  smflimlem2  43196  rmsupp0  44561  rmsuppss  44563  ply1mulgsum  44589  rrxlinesc  44909
  Copyright terms: Public domain W3C validator