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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  f1prex  7282  poxp3  8136  ordiso2  9510  hartogslem1  9537  wemapso2lem  9547  acndom  10046  fin1a2lem12  10406  fin1a2lem13  10407  prlem934  11028  ifle  13176  lcmfunsnlem2lem1  16575  divgcdcoprm0  16602  rpexp  16659  qexpz  16834  ramval  16941  0ram  16953  ramz2  16957  initoeu2lem2  17965  mrelatglb  18513  dfgrp3lem  18921  odbezout  19426  rhmdvdsr  20287  lsmcl  20694  lbsextlem3  20773  frlmsslsp  21351  islindf4  21393  psropprmul  21760  coe1mul2  21791  coe1fzgsumdlem  21825  evl1gsumdlem  21875  scmate  22012  mdetunilem7  22120  mdetmul  22125  cramerlem2  22190  m2pmfzgsumcl  22250  decpmatmul  22274  pmatcollpw3lem  22285  chpdmatlem2  22341  cpmadugsumlemB  22376  cpmadugsumlemC  22377  cpmadugsumlemF  22378  chcoeffeqlem  22387  cnconst2  22787  ordthauslem  22887  clsconn  22934  restnlly  22986  comppfsc  23036  ptpjopn  23116  trfg  23395  rnelfmlem  23456  isfcf  23538  fcfnei  23539  cnpfcf  23545  utop2nei  23755  neipcfilu  23801  blssps  23930  blss  23931  metcnp  24050  xrsxmet  24325  metdsge  24365  metdseq0  24370  addcnlem  24380  xrhmeo  24462  nmhmcn  24636  caucfil  24800  limcfval  25389  fta1b  25687  lgsmod  26826  lgsdir  26835  lgsne0  26838  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd2  27219  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noinfbnd2  27234  scutun12  27311  sltlpss  27401  sleadd1  27472  axpasch  28199  axcontlem2  28223  clwwlknonex2  29362  frgr3v  29528  pjhthmo  30555  difioo  31993  xrge0adddir  32193  archiabl  32344  ssmxidl  32590  dimvalfi  32687  probun  33418  satfv1lem  34353  trisegint  35000  btwnconn1lem13  35071  brsegle2  35081  linethru  35125  lindsadd  36481  hlrelat  38273  intnatN  38278  lnnat  38298  3dim0  38328  3dim1  38338  3dim2  38339  atcvrlln  38391  llnexatN  38392  2at0mat0  38396  llncvrlpln  38429  lplnexllnN  38435  lplncvrlvol  38487  lncvrelatN  38652  lncmp  38654  elpaddn0  38671  paddasslem5  38695  pmapjoin  38723  pmapjat1  38724  pclclN  38762  osumclN  38838  lhprelat3N  38911  trlval4  39059  cdlemd5  39073  cdleme32fvcl  39311  cdleme42keg  39357  cdlemg1a  39441  cdlemg1cN  39458  cdlemg39  39587  ltrncom  39609  cdlemk34  39781  dihord2pre  40096  dihopelvalcpre  40119  dihmeetALTN  40198  dihlspsnssN  40203  dihlspsnat  40204  diophrw  41497  lzunuz  41506  qirropth  41646  jm2.19  41732  jm2.27  41747  lmhmfgsplit  41828  hbtlem5  41870  nadd2rabtr  42134  naddsuc2  42143  fzunt  42206  iunrelexpuztr  42470  rfcnnnub  43720  3adantll2  43725  3adantll3  43726  ioondisj2  44206  ioondisj1  44207  iccintsng  44236  icccncfext  44603  stoweidlem20  44736  stoweidlem61  44777  smflimlem2  45488  rnglidlmcl  46748  rmsupp0  47044  rmsuppss  47046  ply1mulgsum  47071  rrxlinesc  47421