Theorem simpll1 1211

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  f1prex  7156  ordiso2  9274  hartogslem1  9301  wemapso2lem  9311  acndom  9807  fin1a2lem12  10167  fin1a2lem13  10168  prlem934  10789  ifle  12931  lcmfunsnlem2lem1  16343  divgcdcoprm0  16370  rpexp  16427  qexpz  16602  ramval  16709  0ram  16721  ramz2  16725  initoeu2lem2  17730  mrelatglb  18278  dfgrp3lem  18673  odbezout  19165  lsmcl  20345  lbsextlem3  20422  frlmsslsp  21003  islindf4  21045  psropprmul  21409  coe1mul2  21440  coe1fzgsumdlem  21472  evl1gsumdlem  21522  scmate  21659  mdetunilem7  21767  mdetmul  21772  cramerlem2  21837  m2pmfzgsumcl  21897  decpmatmul  21921  pmatcollpw3lem  21932  chpdmatlem2  21988  cpmadugsumlemB  22023  cpmadugsumlemC  22024  cpmadugsumlemF  22025  chcoeffeqlem  22034  cnconst2  22434  ordthauslem  22534  clsconn  22581  restnlly  22633  comppfsc  22683  ptpjopn  22763  trfg  23042  rnelfmlem  23103  isfcf  23185  fcfnei  23186  cnpfcf  23192  utop2nei  23402  neipcfilu  23448  blssps  23577  blss  23578  metcnp  23697  xrsxmet  23972  metdsge  24012  metdseq0  24017  addcnlem  24027  xrhmeo  24109  nmhmcn  24283  caucfil  24447  limcfval  25036  fta1b  25334  lgsmod  26471  lgsdir  26480  lgsne0  26483  axpasch  27309  axcontlem2  27333  clwwlknonex2  28473  frgr3v  28639  pjhthmo  29664  difioo  31103  xrge0adddir  31301  archiabl  31452  rhmdvdsr  31517  ssmxidl  31642  dimvalfi  31687  probun  32386  satfv1lem  33324  nosupbnd1lem3  33913  nosupbnd1lem4  33914  nosupbnd1lem5  33915  nosupbnd2  33919  noinfbnd1lem3  33928  noinfbnd1lem4  33929  noinfbnd1lem5  33930  noinfbnd2  33934  scutun12  34004  sltlpss  34087  trisegint  34330  btwnconn1lem13  34401  brsegle2  34411  linethru  34455  lindsadd  35770  hlrelat  37416  intnatN  37421  lnnat  37441  3dim0  37471  3dim1  37481  3dim2  37482  atcvrlln  37534  llnexatN  37535  2at0mat0  37539  llncvrlpln  37572  lplnexllnN  37578  lplncvrlvol  37630  lncvrelatN  37795  lncmp  37797  elpaddn0  37814  paddasslem5  37838  pmapjoin  37866  pmapjat1  37867  pclclN  37905  osumclN  37981  lhprelat3N  38054  trlval4  38202  cdlemd5  38216  cdleme32fvcl  38454  cdleme42keg  38500  cdlemg1a  38584  cdlemg1cN  38601  cdlemg39  38730  ltrncom  38752  cdlemk34  38924  dihord2pre  39239  dihopelvalcpre  39262  dihmeetALTN  39341  dihlspsnssN  39346  dihlspsnat  39347  diophrw  40581  lzunuz  40590  qirropth  40730  jm2.19  40815  jm2.27  40830  lmhmfgsplit  40911  hbtlem5  40953  fzunt  41062  iunrelexpuztr  41327  rfcnnnub  42579  3adantll2  42586  3adantll3  42587  ioondisj2  43031  ioondisj1  43032  iccintsng  43061  icccncfext  43428  stoweidlem20  43561  stoweidlem61  43602  smflimlem2  44307  rmsupp0  45704  rmsuppss  45706  ply1mulgsum  45731  rrxlinesc  46081