Theorem simpll1 1231

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1prex  7289  poxp3  8152  naddsuc2  8694  ordiso2  9491  hartogslem1  9518  wemapso2lem  9528  acndom  10058  fin1a2lem12  10417  fin1a2lem13  10418  prlem934  11046  ifle  13253  lcmfunsnlem2lem1  16734  divgcdcoprm0  16761  rpexp  16819  qexpz  16999  ramval  17106  0ram  17118  ramz2  17122  initoeu2lem2  18110  mrelatglb  18654  dfgrp3lem  19167  odbezout  19691  rhmdvdsr  20674  lsmcl  21273  lbsextlem3  21353  rnglidlmcl  21410  frlmsslsp  22015  islindf4  22057  psropprmul  22468  coe1mul2  22501  coe1fzgsumdlem  22534  evl1gsumdlem  22587  scmate  22738  mdetunilem7  22846  mdetmul  22851  cramerlem2  22919  m2pmfzgsumcl  22979  decpmatmul  23003  pmatcollpw3lem  23014  chpdmatlem2  23070  cpmadugsumlemB  23105  cpmadugsumlemC  23106  cpmadugsumlemF  23107  chcoeffeqlem  23116  cnconst2  23514  ordthauslem  23614  clsconn  23661  restnlly  23714  comppfsc  23764  ptpjopn  23844  trfg  24123  rnelfmlem  24184  isfcf  24266  fcfnei  24267  cnpfcf  24273  utop2nei  24482  neipcfilu  24527  blssps  24656  blss  24657  metcnp  24773  xrsxmet  25042  metdsge  25082  metdseq0  25087  addcnlem  25097  xrhmeo  25180  nmhmcn  25354  caucfil  25517  limcfval  26106  fta1b  26404  lgsmod  27567  lgsdir  27576  lgsne0  27579  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd2  27960  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  noinfbnd2  27975  cutsun12  28063  ltslpss  28181  leadds1  28262  axpasch  29406  axcontlem2  29430  clwwlknonex2  30587  frgr3v  30763  pjhthmo  31791  difioo  33261  xrge0adddir  33466  archiabl  33646  ssmxidl  33885  dimvalfi  34120  probun  34938  satfv1lem  35949  trisegint  36616  btwnconn1lem13  36687  brsegle2  36697  linethru  36741  lindsadd  38375  hlrelat  40283  intnatN  40288  lnnat  40308  3dim0  40338  3dim1  40348  3dim2  40349  atcvrlln  40401  llnexatN  40402  2at0mat0  40406  llncvrlpln  40439  lplnexllnN  40445  lplncvrlvol  40497  lncvrelatN  40662  lncmp  40664  elpaddn0  40681  paddasslem5  40705  pmapjoin  40733  pmapjat1  40734  pclclN  40772  osumclN  40848  lhprelat3N  40921  trlval4  41069  cdlemd5  41083  cdleme32fvcl  41321  cdleme42keg  41367  cdlemg1a  41451  cdlemg1cN  41468  cdlemg39  41597  ltrncom  41619  cdlemk34  41791  dihord2pre  42106  dihopelvalcpre  42129  dihmeetALTN  42208  dihlspsnssN  42213  dihlspsnat  42214  aks6d1c6isolem1  43048  diophrw  43612  lzunuz  43621  qirropth  43757  jm2.19  43842  jm2.27  43857  lmhmfgsplit  43935  hbtlem5  43977  nadd2rabtr  44233  fzunt  44303  iunrelexpuztr  44567  rfcnnnub  45878  3adantll2  45883  3adantll3  45884  ioondisj2  46331  ioondisj1  46332  iccintsng  46361  icccncfext  46723  stoweidlem20  46856  stoweidlem61  46897  smflimlem2  47608  isuspgrim0lem  48817  isuspgrim0  48818  rmsupp0  49306  rmsuppss  49308  ply1mulgsum  49328  rrxlinesc  49673