Theorem simpll1 1214

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

Step	Hyp	Ref	Expression
1		simp1 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 727	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1prex  7240  poxp3  8102  naddsuc2  8639  ordiso2  9432  hartogslem1  9459  wemapso2lem  9469  acndom  9973  fin1a2lem12  10333  fin1a2lem13  10334  prlem934  10956  ifle  13124  lcmfunsnlem2lem1  16577  divgcdcoprm0  16604  rpexp  16661  qexpz  16841  ramval  16948  0ram  16960  ramz2  16964  initoeu2lem2  17951  mrelatglb  18495  dfgrp3lem  18980  odbezout  19499  rhmdvdsr  20453  lsmcl  21047  lbsextlem3  21127  rnglidlmcl  21183  frlmsslsp  21763  islindf4  21805  psropprmul  22190  coe1mul2  22223  coe1fzgsumdlem  22259  evl1gsumdlem  22312  scmate  22466  mdetunilem7  22574  mdetmul  22579  cramerlem2  22644  m2pmfzgsumcl  22704  decpmatmul  22728  pmatcollpw3lem  22739  chpdmatlem2  22795  cpmadugsumlemB  22830  cpmadugsumlemC  22831  cpmadugsumlemF  22832  chcoeffeqlem  22841  cnconst2  23239  ordthauslem  23339  clsconn  23386  restnlly  23438  comppfsc  23488  ptpjopn  23568  trfg  23847  rnelfmlem  23908  isfcf  23990  fcfnei  23991  cnpfcf  23997  utop2nei  24206  neipcfilu  24251  blssps  24380  blss  24381  metcnp  24497  xrsxmet  24766  metdsge  24806  metdseq0  24811  addcnlem  24821  xrhmeo  24912  nmhmcn  25088  caucfil  25251  limcfval  25841  fta1b  26145  lgsmod  27302  lgsdir  27311  lgsne0  27314  nosupbnd1lem3  27690  nosupbnd1lem4  27691  nosupbnd1lem5  27692  nosupbnd2  27696  noinfbnd1lem3  27705  noinfbnd1lem4  27706  noinfbnd1lem5  27707  noinfbnd2  27711  cutsun12  27798  ltslpss  27916  leadds1  27997  axpasch  29026  axcontlem2  29050  clwwlknonex2  30196  frgr3v  30362  pjhthmo  31389  difioo  32872  xrge0adddir  33110  archiabl  33291  ssmxidl  33566  dimvalfi  33778  probun  34596  satfv1lem  35575  trisegint  36241  btwnconn1lem13  36312  brsegle2  36322  linethru  36366  lindsadd  37858  hlrelat  39772  intnatN  39777  lnnat  39797  3dim0  39827  3dim1  39837  3dim2  39838  atcvrlln  39890  llnexatN  39891  2at0mat0  39895  llncvrlpln  39928  lplnexllnN  39934  lplncvrlvol  39986  lncvrelatN  40151  lncmp  40153  elpaddn0  40170  paddasslem5  40194  pmapjoin  40222  pmapjat1  40223  pclclN  40261  osumclN  40337  lhprelat3N  40410  trlval4  40558  cdlemd5  40572  cdleme32fvcl  40810  cdleme42keg  40856  cdlemg1a  40940  cdlemg1cN  40957  cdlemg39  41086  ltrncom  41108  cdlemk34  41280  dihord2pre  41595  dihopelvalcpre  41618  dihmeetALTN  41697  dihlspsnssN  41702  dihlspsnat  41703  aks6d1c6isolem1  42538  diophrw  43110  lzunuz  43119  qirropth  43259  jm2.19  43344  jm2.27  43359  lmhmfgsplit  43437  hbtlem5  43479  nadd2rabtr  43735  fzunt  43805  iunrelexpuztr  44069  rfcnnnub  45390  3adantll2  45395  3adantll3  45396  ioondisj2  45847  ioondisj1  45848  iccintsng  45877  icccncfext  46239  stoweidlem20  46372  stoweidlem61  46413  smflimlem2  47124  isuspgrim0lem  48247  isuspgrim0  48248  rmsupp0  48722  rmsuppss  48724  ply1mulgsum  48744  rrxlinesc  49089