Theorem simpll1 1210

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

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

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

This theorem is referenced by:  f1prex  7136  ordiso2  9204  hartogslem1  9231  wemapso2lem  9241  acndom  9738  fin1a2lem12  10098  fin1a2lem13  10099  prlem934  10720  ifle  12860  lcmfunsnlem2lem1  16271  divgcdcoprm0  16298  rpexp  16355  qexpz  16530  ramval  16637  0ram  16649  ramz2  16653  initoeu2lem2  17646  mrelatglb  18193  dfgrp3lem  18588  odbezout  19080  lsmcl  20260  lbsextlem3  20337  frlmsslsp  20913  islindf4  20955  psropprmul  21319  coe1mul2  21350  coe1fzgsumdlem  21382  evl1gsumdlem  21432  scmate  21567  mdetunilem7  21675  mdetmul  21680  cramerlem2  21745  m2pmfzgsumcl  21805  decpmatmul  21829  pmatcollpw3lem  21840  chpdmatlem2  21896  cpmadugsumlemB  21931  cpmadugsumlemC  21932  cpmadugsumlemF  21933  chcoeffeqlem  21942  cnconst2  22342  ordthauslem  22442  clsconn  22489  restnlly  22541  comppfsc  22591  ptpjopn  22671  trfg  22950  rnelfmlem  23011  isfcf  23093  fcfnei  23094  cnpfcf  23100  utop2nei  23310  neipcfilu  23356  blssps  23485  blss  23486  metcnp  23603  xrsxmet  23878  metdsge  23918  metdseq0  23923  addcnlem  23933  xrhmeo  24015  nmhmcn  24189  caucfil  24352  limcfval  24941  fta1b  25239  lgsmod  26376  lgsdir  26385  lgsne0  26388  axpasch  27212  axcontlem2  27236  clwwlknonex2  28374  frgr3v  28540  pjhthmo  29565  difioo  31005  xrge0adddir  31203  archiabl  31354  rhmdvdsr  31419  ssmxidl  31544  dimvalfi  31589  probun  32286  satfv1lem  33224  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd2  33846  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd2  33861  scutun12  33931  sltlpss  34014  trisegint  34257  btwnconn1lem13  34328  brsegle2  34338  linethru  34382  lindsadd  35697  hlrelat  37343  intnatN  37348  lnnat  37368  3dim0  37398  3dim1  37408  3dim2  37409  atcvrlln  37461  llnexatN  37462  2at0mat0  37466  llncvrlpln  37499  lplnexllnN  37505  lplncvrlvol  37557  lncvrelatN  37722  lncmp  37724  elpaddn0  37741  paddasslem5  37765  pmapjoin  37793  pmapjat1  37794  pclclN  37832  osumclN  37908  lhprelat3N  37981  trlval4  38129  cdlemd5  38143  cdleme32fvcl  38381  cdleme42keg  38427  cdlemg1a  38511  cdlemg1cN  38528  cdlemg39  38657  ltrncom  38679  cdlemk34  38851  dihord2pre  39166  dihopelvalcpre  39189  dihmeetALTN  39268  dihlspsnssN  39273  dihlspsnat  39274  diophrw  40497  lzunuz  40506  qirropth  40646  jm2.19  40731  jm2.27  40746  lmhmfgsplit  40827  hbtlem5  40869  iunrelexpuztr  41216  rfcnnnub  42468  3adantll2  42475  3adantll3  42476  ioondisj2  42921  ioondisj1  42922  iccintsng  42951  icccncfext  43318  stoweidlem20  43451  stoweidlem61  43492  smflimlem2  44194  rmsupp0  45592  rmsuppss  45594  ply1mulgsum  45619  rrxlinesc  45969