Theorem simpll1 1275

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 1172	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrr 719	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  f1prex  6795  ordiso2  8690  hartogslem1  8717  wemappo  8724  wemapso2lem  8727  acndom  9188  fin1a2lem12  9549  fin1a2lem13  9550  prlem934  10171  ifle  12317  lcmfunsnlem2lem1  15725  divgcdcoprm0  15752  rpexp  15804  qexpz  15977  ramval  16084  0ram  16096  ramz2  16100  initoeu2lem2  17018  mrelatglb  17538  dfgrp3lem  17868  odbezout  18327  lsmcl  19443  lbsextlem3  19522  psropprmul  19969  coe1mul2  20000  coe1fzgsumdlem  20032  evl1gsumdlem  20081  frlmsslsp  20503  islindf4  20545  scmate  20685  mdetunilem7  20793  mdetmul  20798  cramerlem2  20865  m2pmfzgsumcl  20924  decpmatmul  20948  pmatcollpw3lem  20959  chpdmatlem2  21015  cpmadugsumlemB  21050  cpmadugsumlemC  21051  cpmadugsumlemF  21052  chcoeffeqlem  21061  cnconst2  21459  ordthauslem  21559  clsconn  21605  restnlly  21657  comppfsc  21707  ptpjopn  21787  trfg  22066  rnelfmlem  22127  isfcf  22209  fcfnei  22210  cnpfcf  22216  utop2nei  22425  neipcfilu  22471  blssps  22600  blss  22601  metcnp  22717  xrsxmet  22983  metdsge  23023  metdseq0  23028  addcnlem  23038  xrhmeo  23116  nmhmcn  23290  caucfil  23452  limcfval  24036  fta1b  24329  lgsmod  25462  lgsdir  25471  lgsne0  25474  axpasch  26241  axcontlem2  26265  clwwlknonex2  27485  frgr3v  27657  pjhthmo  28717  difioo  30092  xrge0adddir  30238  archiabl  30298  rhmdvdsr  30364  probun  31028  nosupbnd1lem3  32396  nosupbnd1lem4  32397  nosupbnd1lem5  32398  nosupbnd2  32402  scutun12  32457  trisegint  32675  btwnconn1lem13  32746  brsegle2  32756  linethru  32800  lindsadd  33947  hlrelat  35478  intnatN  35483  lnnat  35503  3dim0  35533  3dim1  35543  3dim2  35544  atcvrlln  35596  llnexatN  35597  2at0mat0  35601  llncvrlpln  35634  lplnexllnN  35640  lplncvrlvol  35692  lncvrelatN  35857  lncmp  35859  elpaddn0  35876  paddasslem5  35900  pmapjoin  35928  pmapjat1  35929  pclclN  35967  osumclN  36043  lhprelat3N  36116  trlval4  36264  cdlemd5  36278  cdleme32fvcl  36516  cdleme42keg  36562  cdlemg1a  36646  cdlemg1cN  36663  cdlemg39  36792  ltrncom  36814  cdlemk34  36986  dihord2pre  37301  dihopelvalcpre  37324  dihmeetALTN  37403  dihlspsnssN  37408  dihlspsnat  37409  diophrw  38167  lzunuz  38176  qirropth  38317  jm2.19  38404  jm2.27  38419  lmhmfgsplit  38500  hbtlem5  38542  iunrelexpuztr  38853  rfcnnnub  40014  3adantll2  40021  3adantll3  40022  ioondisj2  40514  ioondisj1  40515  iccintsng  40546  icccncfext  40896  stoweidlem20  41032  stoweidlem61  41073  smflimlem2  41775  rmsupp0  42997  rmsuppss  42999  ply1mulgsum  43026  rrxlinesc  43287