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  7218  poxp3  8080  naddsuc2  8616  ordiso2  9401  hartogslem1  9428  wemapso2lem  9438  acndom  9942  fin1a2lem12  10302  fin1a2lem13  10303  prlem934  10924  ifle  13096  lcmfunsnlem2lem1  16549  divgcdcoprm0  16576  rpexp  16633  qexpz  16813  ramval  16920  0ram  16932  ramz2  16936  initoeu2lem2  17922  mrelatglb  18466  dfgrp3lem  18951  odbezout  19471  rhmdvdsr  20424  lsmcl  21018  lbsextlem3  21098  rnglidlmcl  21154  frlmsslsp  21734  islindf4  21776  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  28920  axcontlem2  28944  clwwlknonex2  30087  frgr3v  30253  pjhthmo  31280  difioo  32763  xrge0adddir  32997  archiabl  33165  ssmxidl  33437  dimvalfi  33612  probun  34430  satfv1lem  35404  trisegint  36068  btwnconn1lem13  36139  brsegle2  36149  linethru  36193  lindsadd  37659  hlrelat  39447  intnatN  39452  lnnat  39472  3dim0  39502  3dim1  39512  3dim2  39513  atcvrlln  39565  llnexatN  39566  2at0mat0  39570  llncvrlpln  39603  lplnexllnN  39609  lplncvrlvol  39661  lncvrelatN  39826  lncmp  39828  elpaddn0  39845  paddasslem5  39869  pmapjoin  39897  pmapjat1  39898  pclclN  39936  osumclN  40012  lhprelat3N  40085  trlval4  40233  cdlemd5  40247  cdleme32fvcl  40485  cdleme42keg  40531  cdlemg1a  40615  cdlemg1cN  40632  cdlemg39  40761  ltrncom  40783  cdlemk34  40955  dihord2pre  41270  dihopelvalcpre  41293  dihmeetALTN  41372  dihlspsnssN  41377  dihlspsnat  41378  aks6d1c6isolem1  42213  diophrw  42798  lzunuz  42807  qirropth  42947  jm2.19  43032  jm2.27  43047  lmhmfgsplit  43125  hbtlem5  43167  nadd2rabtr  43423  fzunt  43494  iunrelexpuztr  43758  rfcnnnub  45079  3adantll2  45084  3adantll3  45085  ioondisj2  45539  ioondisj1  45540  iccintsng  45569  icccncfext  45931  stoweidlem20  46064  stoweidlem61  46105  smflimlem2  46816  isuspgrim0lem  47930  isuspgrim0  47931  rmsupp0  48405  rmsuppss  48407  ply1mulgsum  48428  rrxlinesc  48773