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  7276  poxp3  8147  naddsuc2  8711  ordiso2  9527  hartogslem1  9554  wemapso2lem  9564  acndom  10063  fin1a2lem12  10423  fin1a2lem13  10424  prlem934  11045  ifle  13211  lcmfunsnlem2lem1  16655  divgcdcoprm0  16682  rpexp  16739  qexpz  16919  ramval  17026  0ram  17038  ramz2  17042  initoeu2lem2  18026  mrelatglb  18568  dfgrp3lem  19019  odbezout  19537  rhmdvdsr  20466  lsmcl  21039  lbsextlem3  21119  rnglidlmcl  21175  frlmsslsp  21754  islindf4  21796  psropprmul  22171  coe1mul2  22204  coe1fzgsumdlem  22239  evl1gsumdlem  22292  scmate  22446  mdetunilem7  22554  mdetmul  22559  cramerlem2  22624  m2pmfzgsumcl  22684  decpmatmul  22708  pmatcollpw3lem  22719  chpdmatlem2  22775  cpmadugsumlemB  22810  cpmadugsumlemC  22811  cpmadugsumlemF  22812  chcoeffeqlem  22821  cnconst2  23219  ordthauslem  23319  clsconn  23366  restnlly  23418  comppfsc  23468  ptpjopn  23548  trfg  23827  rnelfmlem  23888  isfcf  23970  fcfnei  23971  cnpfcf  23977  utop2nei  24187  neipcfilu  24232  blssps  24361  blss  24362  metcnp  24478  xrsxmet  24747  metdsge  24787  metdseq0  24792  addcnlem  24802  xrhmeo  24893  nmhmcn  25069  caucfil  25233  limcfval  25823  fta1b  26127  lgsmod  27284  lgsdir  27293  lgsne0  27296  nosupbnd1lem3  27672  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd2  27678  noinfbnd1lem3  27687  noinfbnd1lem4  27688  noinfbnd1lem5  27689  noinfbnd2  27693  scutun12  27772  sltlpss  27862  sleadd1  27939  axpasch  28866  axcontlem2  28890  clwwlknonex2  30036  frgr3v  30202  pjhthmo  31229  difioo  32705  xrge0adddir  32959  archiabl  33142  ssmxidl  33435  dimvalfi  33587  probun  34397  satfv1lem  35330  trisegint  35992  btwnconn1lem13  36063  brsegle2  36073  linethru  36117  lindsadd  37583  hlrelat  39367  intnatN  39372  lnnat  39392  3dim0  39422  3dim1  39432  3dim2  39433  atcvrlln  39485  llnexatN  39486  2at0mat0  39490  llncvrlpln  39523  lplnexllnN  39529  lplncvrlvol  39581  lncvrelatN  39746  lncmp  39748  elpaddn0  39765  paddasslem5  39789  pmapjoin  39817  pmapjat1  39818  pclclN  39856  osumclN  39932  lhprelat3N  40005  trlval4  40153  cdlemd5  40167  cdleme32fvcl  40405  cdleme42keg  40451  cdlemg1a  40535  cdlemg1cN  40552  cdlemg39  40681  ltrncom  40703  cdlemk34  40875  dihord2pre  41190  dihopelvalcpre  41213  dihmeetALTN  41292  dihlspsnssN  41297  dihlspsnat  41298  aks6d1c6isolem1  42133  diophrw  42729  lzunuz  42738  qirropth  42878  jm2.19  42964  jm2.27  42979  lmhmfgsplit  43057  hbtlem5  43099  nadd2rabtr  43355  fzunt  43426  iunrelexpuztr  43690  rfcnnnub  45008  3adantll2  45013  3adantll3  45014  ioondisj2  45470  ioondisj1  45471  iccintsng  45500  icccncfext  45864  stoweidlem20  45997  stoweidlem61  46038  smflimlem2  46749  isuspgrim0lem  47854  isuspgrim0  47855  rmsupp0  48291  rmsuppss  48293  ply1mulgsum  48314  rrxlinesc  48663