Theorem simpll1 1211

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 1135	. 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  7303  poxp3  8173  naddsuc2  8737  ordiso2  9552  hartogslem1  9579  wemapso2lem  9589  acndom  10088  fin1a2lem12  10448  fin1a2lem13  10449  prlem934  11070  ifle  13235  lcmfunsnlem2lem1  16671  divgcdcoprm0  16698  rpexp  16755  qexpz  16934  ramval  17041  0ram  17053  ramz2  17057  initoeu2lem2  18068  mrelatglb  18617  dfgrp3lem  19068  odbezout  19590  rhmdvdsr  20524  lsmcl  21099  lbsextlem3  21179  rnglidlmcl  21243  frlmsslsp  21833  islindf4  21875  psropprmul  22254  coe1mul2  22287  coe1fzgsumdlem  22322  evl1gsumdlem  22375  scmate  22531  mdetunilem7  22639  mdetmul  22644  cramerlem2  22709  m2pmfzgsumcl  22769  decpmatmul  22793  pmatcollpw3lem  22804  chpdmatlem2  22860  cpmadugsumlemB  22895  cpmadugsumlemC  22896  cpmadugsumlemF  22897  chcoeffeqlem  22906  cnconst2  23306  ordthauslem  23406  clsconn  23453  restnlly  23505  comppfsc  23555  ptpjopn  23635  trfg  23914  rnelfmlem  23975  isfcf  24057  fcfnei  24058  cnpfcf  24064  utop2nei  24274  neipcfilu  24320  blssps  24449  blss  24450  metcnp  24569  xrsxmet  24844  metdsge  24884  metdseq0  24889  addcnlem  24899  xrhmeo  24990  nmhmcn  25166  caucfil  25330  limcfval  25921  fta1b  26225  lgsmod  27381  lgsdir  27390  lgsne0  27393  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd2  27775  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noinfbnd2  27790  scutun12  27869  sltlpss  27959  sleadd1  28036  axpasch  28970  axcontlem2  28994  clwwlknonex2  30137  frgr3v  30303  pjhthmo  31330  difioo  32790  xrge0adddir  33005  archiabl  33187  ssmxidl  33481  dimvalfi  33628  probun  34400  satfv1lem  35346  trisegint  36009  btwnconn1lem13  36080  brsegle2  36090  linethru  36134  lindsadd  37599  hlrelat  39384  intnatN  39389  lnnat  39409  3dim0  39439  3dim1  39449  3dim2  39450  atcvrlln  39502  llnexatN  39503  2at0mat0  39507  llncvrlpln  39540  lplnexllnN  39546  lplncvrlvol  39598  lncvrelatN  39763  lncmp  39765  elpaddn0  39782  paddasslem5  39806  pmapjoin  39834  pmapjat1  39835  pclclN  39873  osumclN  39949  lhprelat3N  40022  trlval4  40170  cdlemd5  40184  cdleme32fvcl  40422  cdleme42keg  40468  cdlemg1a  40552  cdlemg1cN  40569  cdlemg39  40698  ltrncom  40720  cdlemk34  40892  dihord2pre  41207  dihopelvalcpre  41230  dihmeetALTN  41309  dihlspsnssN  41314  dihlspsnat  41315  aks6d1c6isolem1  42155  diophrw  42746  lzunuz  42755  qirropth  42895  jm2.19  42981  jm2.27  42996  lmhmfgsplit  43074  hbtlem5  43116  nadd2rabtr  43373  fzunt  43444  iunrelexpuztr  43708  rfcnnnub  44973  3adantll2  44978  3adantll3  44979  ioondisj2  45445  ioondisj1  45446  iccintsng  45475  icccncfext  45842  stoweidlem20  45975  stoweidlem61  46016  smflimlem2  46727  isuspgrim0lem  47808  isuspgrim0  47809  rmsupp0  48212  rmsuppss  48214  ply1mulgsum  48235  rrxlinesc  48584