Theorem simpll1 1214

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 727	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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

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 1089

This theorem is referenced by:  f1prex  7239  poxp3  8100  naddsuc2  8637  ordiso2  9430  hartogslem1  9457  wemapso2lem  9467  acndom  9973  fin1a2lem12  10333  fin1a2lem13  10334  prlem934  10956  ifle  13149  lcmfunsnlem2lem1  16607  divgcdcoprm0  16634  rpexp  16692  qexpz  16872  ramval  16979  0ram  16991  ramz2  16995  initoeu2lem2  17982  mrelatglb  18526  dfgrp3lem  19014  odbezout  19533  rhmdvdsr  20485  lsmcl  21078  lbsextlem3  21158  rnglidlmcl  21214  frlmsslsp  21776  islindf4  21818  psropprmul  22201  coe1mul2  22234  coe1fzgsumdlem  22268  evl1gsumdlem  22321  scmate  22475  mdetunilem7  22583  mdetmul  22588  cramerlem2  22653  m2pmfzgsumcl  22713  decpmatmul  22737  pmatcollpw3lem  22748  chpdmatlem2  22804  cpmadugsumlemB  22839  cpmadugsumlemC  22840  cpmadugsumlemF  22841  chcoeffeqlem  22850  cnconst2  23248  ordthauslem  23348  clsconn  23395  restnlly  23447  comppfsc  23497  ptpjopn  23577  trfg  23856  rnelfmlem  23917  isfcf  23999  fcfnei  24000  cnpfcf  24006  utop2nei  24215  neipcfilu  24260  blssps  24389  blss  24390  metcnp  24506  xrsxmet  24775  metdsge  24815  metdseq0  24820  addcnlem  24830  xrhmeo  24913  nmhmcn  25087  caucfil  25250  limcfval  25839  fta1b  26137  lgsmod  27286  lgsdir  27295  lgsne0  27298  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd2  27680  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd2  27695  cutsun12  27782  ltslpss  27900  leadds1  27981  axpasch  29010  axcontlem2  29034  clwwlknonex2  30179  frgr3v  30345  pjhthmo  31373  difioo  32855  xrge0adddir  33078  archiabl  33259  ssmxidl  33534  dimvalfi  33746  probun  34563  satfv1lem  35544  trisegint  36210  btwnconn1lem13  36281  brsegle2  36291  linethru  36335  lindsadd  37934  hlrelat  39848  intnatN  39853  lnnat  39873  3dim0  39903  3dim1  39913  3dim2  39914  atcvrlln  39966  llnexatN  39967  2at0mat0  39971  llncvrlpln  40004  lplnexllnN  40010  lplncvrlvol  40062  lncvrelatN  40227  lncmp  40229  elpaddn0  40246  paddasslem5  40270  pmapjoin  40298  pmapjat1  40299  pclclN  40337  osumclN  40413  lhprelat3N  40486  trlval4  40634  cdlemd5  40648  cdleme32fvcl  40886  cdleme42keg  40932  cdlemg1a  41016  cdlemg1cN  41033  cdlemg39  41162  ltrncom  41184  cdlemk34  41356  dihord2pre  41671  dihopelvalcpre  41694  dihmeetALTN  41773  dihlspsnssN  41778  dihlspsnat  41779  aks6d1c6isolem1  42613  diophrw  43191  lzunuz  43200  qirropth  43336  jm2.19  43421  jm2.27  43436  lmhmfgsplit  43514  hbtlem5  43556  nadd2rabtr  43812  fzunt  43882  iunrelexpuztr  44146  rfcnnnub  45467  3adantll2  45472  3adantll3  45473  ioondisj2  45923  ioondisj1  45924  iccintsng  45953  icccncfext  46315  stoweidlem20  46448  stoweidlem61  46489  smflimlem2  47200  isuspgrim0lem  48369  isuspgrim0  48370  rmsupp0  48844  rmsuppss  48846  ply1mulgsum  48866  rrxlinesc  49211