Theorem simpll1 1269

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1107

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 198  df-an 385  df-3an 1109

This theorem is referenced by:  f1prex  6731  ordiso2  8627  hartogslem1  8654  wemappo  8661  wemapso2lem  8664  acndom  9125  fin1a2lem12  9486  fin1a2lem13  9487  prlem934  10108  ifle  12230  lcmfunsnlem2lem1  15634  divgcdcoprm0  15661  rpexp  15713  qexpz  15886  ramval  15993  0ram  16005  ramz2  16009  initoeu2lem2  16932  mrelatglb  17452  dfgrp3lem  17782  odbezout  18241  lsmcl  19355  lbsextlem3  19434  psropprmul  19881  coe1mul2  19912  coe1fzgsumdlem  19944  evl1gsumdlem  19993  frlmsslsp  20411  islindf4  20453  scmate  20593  mdetunilem7  20701  mdetmul  20706  cramerlem2  20773  m2pmfzgsumcl  20832  decpmatmul  20856  pmatcollpw3lem  20867  chpdmatlem2  20923  cpmadugsumlemB  20958  cpmadugsumlemC  20959  cpmadugsumlemF  20960  chcoeffeqlem  20969  cnconst2  21367  ordthauslem  21467  clsconn  21513  restnlly  21565  comppfsc  21615  ptpjopn  21695  trfg  21974  rnelfmlem  22035  isfcf  22117  fcfnei  22118  cnpfcf  22124  utop2nei  22333  neipcfilu  22379  blssps  22508  blss  22509  metcnp  22625  xrsxmet  22891  metdsge  22931  metdseq0  22936  addcnlem  22946  xrhmeo  23024  nmhmcn  23198  caucfil  23360  limcfval  23927  fta1b  24220  lgsmod  25339  lgsdir  25348  lgsne0  25351  axpasch  26112  axcontlem2  26136  wpthswwlks2onOLD  27166  clwwlknonex2  27341  frgr3v  27513  pjhthmo  28552  difioo  29928  xrge0adddir  30074  archiabl  30134  rhmdvdsr  30200  probun  30864  nosupbnd1lem3  32232  nosupbnd1lem4  32233  nosupbnd1lem5  32234  nosupbnd2  32238  scutun12  32293  trisegint  32511  btwnconn1lem13  32582  brsegle2  32592  linethru  32636  hlrelat  35290  intnatN  35295  lnnat  35315  3dim0  35345  3dim1  35355  3dim2  35356  atcvrlln  35408  llnexatN  35409  2at0mat0  35413  llncvrlpln  35446  lplnexllnN  35452  lplncvrlvol  35504  lncvrelatN  35669  lncmp  35671  elpaddn0  35688  paddasslem5  35712  pmapjoin  35740  pmapjat1  35741  pclclN  35779  osumclN  35855  lhprelat3N  35928  trlval4  36076  cdlemd5  36090  cdleme32fvcl  36328  cdleme42keg  36374  cdlemg1a  36458  cdlemg1cN  36475  cdlemg39  36604  ltrncom  36626  cdlemk34  36798  dihord2pre  37113  dihopelvalcpre  37136  dihmeetALTN  37215  dihlspsnssN  37220  dihlspsnat  37221  diophrw  37932  lzunuz  37941  qirropth  38082  jm2.19  38169  jm2.27  38184  lmhmfgsplit  38265  hbtlem5  38307  iunrelexpuztr  38618  rfcnnnub  39779  3adantll2  39786  3adantll3  39787  ioondisj2  40288  ioondisj1  40289  iccintsng  40320  icccncfext  40670  stoweidlem20  40806  stoweidlem61  40847  smflimlem2  41552  rmsupp0  42750  rmsuppss  42752  ply1mulgsum  42779