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

Theorem simpll1 1213
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 1137 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antrr 725 1 ((((𝜑𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 206  df-an 398  df-3an 1090
This theorem is referenced by:  f1prex  7234  poxp3  8086  ordiso2  9459  hartogslem1  9486  wemapso2lem  9496  acndom  9995  fin1a2lem12  10355  fin1a2lem13  10356  prlem934  10977  ifle  13125  lcmfunsnlem2lem1  16522  divgcdcoprm0  16549  rpexp  16606  qexpz  16781  ramval  16888  0ram  16900  ramz2  16904  initoeu2lem2  17909  mrelatglb  18457  dfgrp3lem  18853  odbezout  19348  rhmdvdsr  20191  lsmcl  20588  lbsextlem3  20666  frlmsslsp  21225  islindf4  21267  psropprmul  21632  coe1mul2  21663  coe1fzgsumdlem  21695  evl1gsumdlem  21745  scmate  21882  mdetunilem7  21990  mdetmul  21995  cramerlem2  22060  m2pmfzgsumcl  22120  decpmatmul  22144  pmatcollpw3lem  22155  chpdmatlem2  22211  cpmadugsumlemB  22246  cpmadugsumlemC  22247  cpmadugsumlemF  22248  chcoeffeqlem  22257  cnconst2  22657  ordthauslem  22757  clsconn  22804  restnlly  22856  comppfsc  22906  ptpjopn  22986  trfg  23265  rnelfmlem  23326  isfcf  23408  fcfnei  23409  cnpfcf  23415  utop2nei  23625  neipcfilu  23671  blssps  23800  blss  23801  metcnp  23920  xrsxmet  24195  metdsge  24235  metdseq0  24240  addcnlem  24250  xrhmeo  24332  nmhmcn  24506  caucfil  24670  limcfval  25259  fta1b  25557  lgsmod  26694  lgsdir  26703  lgsne0  26706  nosupbnd1lem3  27081  nosupbnd1lem4  27082  nosupbnd1lem5  27083  nosupbnd2  27087  noinfbnd1lem3  27096  noinfbnd1lem4  27097  noinfbnd1lem5  27098  noinfbnd2  27102  scutun12  27178  sltlpss  27265  sleadd1  27327  axpasch  27939  axcontlem2  27963  clwwlknonex2  29102  frgr3v  29268  pjhthmo  30293  difioo  31739  xrge0adddir  31939  archiabl  32090  ssmxidl  32294  dimvalfi  32363  probun  33083  satfv1lem  34020  trisegint  34666  btwnconn1lem13  34737  brsegle2  34747  linethru  34791  lindsadd  36121  hlrelat  37915  intnatN  37920  lnnat  37940  3dim0  37970  3dim1  37980  3dim2  37981  atcvrlln  38033  llnexatN  38034  2at0mat0  38038  llncvrlpln  38071  lplnexllnN  38077  lplncvrlvol  38129  lncvrelatN  38294  lncmp  38296  elpaddn0  38313  paddasslem5  38337  pmapjoin  38365  pmapjat1  38366  pclclN  38404  osumclN  38480  lhprelat3N  38553  trlval4  38701  cdlemd5  38715  cdleme32fvcl  38953  cdleme42keg  38999  cdlemg1a  39083  cdlemg1cN  39100  cdlemg39  39229  ltrncom  39251  cdlemk34  39423  dihord2pre  39738  dihopelvalcpre  39761  dihmeetALTN  39840  dihlspsnssN  39845  dihlspsnat  39846  diophrw  41129  lzunuz  41138  qirropth  41278  jm2.19  41364  jm2.27  41379  lmhmfgsplit  41460  hbtlem5  41502  nadd2rabtr  41747  naddsuc2  41756  fzunt  41819  iunrelexpuztr  42083  rfcnnnub  43333  3adantll2  43338  3adantll3  43339  ioondisj2  43821  ioondisj1  43822  iccintsng  43851  icccncfext  44218  stoweidlem20  44351  stoweidlem61  44392  smflimlem2  45103  rmsupp0  46534  rmsuppss  46536  ply1mulgsum  46561  rrxlinesc  46911
  Copyright terms: Public domain W3C validator