Theorem simpl1l 1225

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 766	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1186	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:  soisores  7320  tfisi  7854  funelss  8046  omopth2  8596  swrdsbslen  14682  swrdspsleq  14683  repswswrd  14802  ramub1lem1  17046  cntzsubrng  20527  cntzsubr  20566  lbspss  21040  maducoeval2  22578  cramer  22629  neiptopnei  23070  ptbasin  23515  basqtop  23649  tmdgsum  24033  ustuqtop1  24180  cxplea  26657  cxple2  26658  nosupbnd2lem1  27679  noinfbnd2lem1  27694  sltmul2  28126  ewlkle  29585  uspgr2wlkeq2  29627  clwwlkccat  29971  br8d  32590  isarchi2  33183  archiabllem2c  33193  cvmlift2lem10  35334  5segofs  36024  2llnjaN  39585  lvolnle3at  39601  paddasslem12  39850  paddasslem13  39851  atmod1i1m  39877  lhp2lt  40020  lhpexle2lem  40028  lhpmcvr3  40044  lhpat3  40065  ltrneq2  40167  trlnle  40205  trlval3  40206  trlval4  40207  cdleme0moN  40244  cdleme17b  40306  cdlemefrs29pre00  40414  cdlemefr27cl  40422  cdleme42ke  40504  cdleme42mgN  40507  cdleme46f2g2  40512  cdleme46f2g1  40513  cdleme50eq  40560  cdleme50trn3  40572  trlord  40588  cdlemg6c  40639  cdlemg11b  40661  cdlemg18a  40697  cdlemg42  40748  cdlemg46  40754  trljco  40759  tendococl  40791  cdlemj3  40842  tendotr  40849  cdlemk35s-id  40957  cdlemk39s-id  40959  cdlemk53b  40975  cdlemk53  40976  cdlemk35u  40983  tendoex  40994  cdlemm10N  41137  dihopelvalcpre  41267  dihord6apre  41275  dihord5b  41278  dihglblem5apreN  41310  dihglblem2N  41313  dihmeetlem4preN  41325  dihmeetlem6  41328  dihmeetlem10N  41335  dihmeetlem11N  41336  dihmeetlem16N  41341  dihmeetlem17N  41342  dihmeetlem18N  41343  dihmeetlem19N  41344  dihmeetALTN  41346  dihlspsnat  41352  dvh3dim2  41467  dvh3dim3N  41468  jm2.25lem1  43022  jm2.26  43026  grur1cld  44256  limcperiod  45657  0ellimcdiv  45678  cncfshift  45903  cncfperiod  45908  icccncfext  45916  stoweidlem34  46063  fourierdlem48  46183  fourierdlem87  46222  sge0xaddlem2  46463  smflimsuplem7  46855  domnmsuppn0  48344  itscnhlinecirc02plem2  48763