Theorem simpl1l 1226

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simpl1l	⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Proof of Theorem simpl1l

Step	Hyp	Ref	Expression
1		simpll 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1187	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:  soisores  7283  tfisi  7811  funelss  8001  omopth2  8521  swrdsbslen  14600  swrdspsleq  14601  repswswrd  14719  ramub1lem1  16966  cntzsubrng  20512  cntzsubr  20551  lbspss  21046  maducoeval2  22596  cramer  22647  neiptopnei  23088  ptbasin  23533  basqtop  23667  tmdgsum  24051  ustuqtop1  24197  cxplea  26673  cxple2  26674  nosupbnd2lem1  27695  noinfbnd2lem1  27710  ltmuls2  28179  ewlkle  29691  uspgr2wlkeq2  29732  clwwlkccat  30077  br8d  32697  isarchi2  33278  archiabllem2c  33288  cvmlift2lem10  35525  5segofs  36219  2llnjaN  39936  lvolnle3at  39952  paddasslem12  40201  paddasslem13  40202  atmod1i1m  40228  lhp2lt  40371  lhpexle2lem  40379  lhpmcvr3  40395  lhpat3  40416  ltrneq2  40518  trlnle  40556  trlval3  40557  trlval4  40558  cdleme0moN  40595  cdleme17b  40657  cdlemefrs29pre00  40765  cdlemefr27cl  40773  cdleme42ke  40855  cdleme42mgN  40858  cdleme46f2g2  40863  cdleme46f2g1  40864  cdleme50eq  40911  cdleme50trn3  40923  trlord  40939  cdlemg6c  40990  cdlemg11b  41012  cdlemg18a  41048  cdlemg42  41099  cdlemg46  41105  trljco  41110  tendococl  41142  cdlemj3  41193  tendotr  41200  cdlemk35s-id  41308  cdlemk39s-id  41310  cdlemk53b  41326  cdlemk53  41327  cdlemk35u  41334  tendoex  41345  cdlemm10N  41488  dihopelvalcpre  41618  dihord6apre  41626  dihord5b  41629  dihglblem5apreN  41661  dihglblem2N  41664  dihmeetlem4preN  41676  dihmeetlem6  41679  dihmeetlem10N  41686  dihmeetlem11N  41687  dihmeetlem16N  41692  dihmeetlem17N  41693  dihmeetlem18N  41694  dihmeetlem19N  41695  dihmeetALTN  41697  dihlspsnat  41703  dvh3dim2  41818  dvh3dim3N  41819  jm2.25lem1  43349  jm2.26  43353  grur1cld  44582  limcperiod  45982  0ellimcdiv  46001  cncfshift  46226  cncfperiod  46231  icccncfext  46239  stoweidlem34  46386  fourierdlem48  46506  fourierdlem87  46545  sge0xaddlem2  46786  smflimsuplem7  47178  domnmsuppn0  48723  itscnhlinecirc02plem2  49137