Theorem simpl1l 1224

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 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜑)
2	1	3ad2antl1 1185	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  soisores  7323  tfisi  7847  funelss  8032  omopth2  8583  swrdsbslen  14613  swrdspsleq  14614  repswswrd  14733  ramub1lem1  16958  cntzsubr  20352  lbspss  20692  maducoeval2  22141  cramer  22192  neiptopnei  22635  ptbasin  23080  basqtop  23214  tmdgsum  23598  ustuqtop1  23745  cxplea  26203  cxple2  26204  nosupbnd2lem1  27215  noinfbnd2lem1  27230  sltmul2  27620  ewlkle  28859  uspgr2wlkeq2  28901  clwwlkccat  29240  br8d  31834  isarchi2  32326  archiabllem2c  32336  cvmlift2lem10  34298  5segofs  34973  2llnjaN  38432  lvolnle3at  38448  paddasslem12  38697  paddasslem13  38698  atmod1i1m  38724  lhp2lt  38867  lhpexle2lem  38875  lhpmcvr3  38891  lhpat3  38912  ltrneq2  39014  trlnle  39052  trlval3  39053  trlval4  39054  cdleme0moN  39091  cdleme17b  39153  cdlemefrs29pre00  39261  cdlemefr27cl  39269  cdleme42ke  39351  cdleme42mgN  39354  cdleme46f2g2  39359  cdleme46f2g1  39360  cdleme50eq  39407  cdleme50trn3  39419  trlord  39435  cdlemg6c  39486  cdlemg11b  39508  cdlemg18a  39544  cdlemg42  39595  cdlemg46  39601  trljco  39606  tendococl  39638  cdlemj3  39689  tendotr  39696  cdlemk35s-id  39804  cdlemk39s-id  39806  cdlemk53b  39822  cdlemk53  39823  cdlemk35u  39830  tendoex  39841  cdlemm10N  39984  dihopelvalcpre  40114  dihord6apre  40122  dihord5b  40125  dihglblem5apreN  40157  dihglblem2N  40160  dihmeetlem4preN  40172  dihmeetlem6  40175  dihmeetlem10N  40182  dihmeetlem11N  40183  dihmeetlem16N  40188  dihmeetlem17N  40189  dihmeetlem18N  40190  dihmeetlem19N  40191  dihmeetALTN  40193  dihlspsnat  40199  dvh3dim2  40314  dvh3dim3N  40315  jm2.25lem1  41727  jm2.26  41731  grur1cld  42981  limcperiod  44334  0ellimcdiv  44355  cncfshift  44580  cncfperiod  44585  icccncfext  44593  stoweidlem34  44740  fourierdlem48  44860  fourierdlem87  44899  sge0xaddlem2  45140  smflimsuplem7  45532  isomgrsym  46494  cntzsubrng  46736  domnmsuppn0  47035  itscnhlinecirc02plem2  47459