Theorem simpll1 1213

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1prex  7224  poxp3  8086  naddsuc2  8622  ordiso2  9408  hartogslem1  9435  wemapso2lem  9445  acndom  9949  fin1a2lem12  10309  fin1a2lem13  10310  prlem934  10931  ifle  13098  lcmfunsnlem2lem1  16551  divgcdcoprm0  16578  rpexp  16635  qexpz  16815  ramval  16922  0ram  16934  ramz2  16938  initoeu2lem2  17924  mrelatglb  18468  dfgrp3lem  18953  odbezout  19472  rhmdvdsr  20425  lsmcl  21019  lbsextlem3  21099  rnglidlmcl  21155  frlmsslsp  21735  islindf4  21777  psropprmul  22151  coe1mul2  22184  coe1fzgsumdlem  22219  evl1gsumdlem  22272  scmate  22426  mdetunilem7  22534  mdetmul  22539  cramerlem2  22604  m2pmfzgsumcl  22664  decpmatmul  22688  pmatcollpw3lem  22699  chpdmatlem2  22755  cpmadugsumlemB  22790  cpmadugsumlemC  22791  cpmadugsumlemF  22792  chcoeffeqlem  22801  cnconst2  23199  ordthauslem  23299  clsconn  23346  restnlly  23398  comppfsc  23448  ptpjopn  23528  trfg  23807  rnelfmlem  23868  isfcf  23950  fcfnei  23951  cnpfcf  23957  utop2nei  24166  neipcfilu  24211  blssps  24340  blss  24341  metcnp  24457  xrsxmet  24726  metdsge  24766  metdseq0  24771  addcnlem  24781  xrhmeo  24872  nmhmcn  25048  caucfil  25211  limcfval  25801  fta1b  26105  lgsmod  27262  lgsdir  27271  lgsne0  27274  nosupbnd1lem3  27650  nosupbnd1lem4  27651  nosupbnd1lem5  27652  nosupbnd2  27656  noinfbnd1lem3  27665  noinfbnd1lem4  27666  noinfbnd1lem5  27667  noinfbnd2  27671  scutun12  27752  sltlpss  27854  sleadd1  27933  axpasch  28921  axcontlem2  28945  clwwlknonex2  30091  frgr3v  30257  pjhthmo  31284  difioo  32769  xrge0adddir  33006  archiabl  33174  ssmxidl  33446  dimvalfi  33635  probun  34453  satfv1lem  35427  trisegint  36093  btwnconn1lem13  36164  brsegle2  36174  linethru  36218  lindsadd  37674  hlrelat  39522  intnatN  39527  lnnat  39547  3dim0  39577  3dim1  39587  3dim2  39588  atcvrlln  39640  llnexatN  39641  2at0mat0  39645  llncvrlpln  39678  lplnexllnN  39684  lplncvrlvol  39736  lncvrelatN  39901  lncmp  39903  elpaddn0  39920  paddasslem5  39944  pmapjoin  39972  pmapjat1  39973  pclclN  40011  osumclN  40087  lhprelat3N  40160  trlval4  40308  cdlemd5  40322  cdleme32fvcl  40560  cdleme42keg  40606  cdlemg1a  40690  cdlemg1cN  40707  cdlemg39  40836  ltrncom  40858  cdlemk34  41030  dihord2pre  41345  dihopelvalcpre  41368  dihmeetALTN  41447  dihlspsnssN  41452  dihlspsnat  41453  aks6d1c6isolem1  42288  diophrw  42877  lzunuz  42886  qirropth  43026  jm2.19  43111  jm2.27  43126  lmhmfgsplit  43204  hbtlem5  43246  nadd2rabtr  43502  fzunt  43573  iunrelexpuztr  43837  rfcnnnub  45158  3adantll2  45163  3adantll3  45164  ioondisj2  45618  ioondisj1  45619  iccintsng  45648  icccncfext  46010  stoweidlem20  46143  stoweidlem61  46184  smflimlem2  46895  isuspgrim0lem  48018  isuspgrim0  48019  rmsupp0  48493  rmsuppss  48495  ply1mulgsum  48516  rrxlinesc  48861