Theorem simpl1l 1112

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

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

Proof of Theorem simpl1l

Step	Hyp	Ref	Expression
1		simp1l 1085	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) → 𝜑)
2	1	adantr 481	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  soisores  6577  tfisi  7058  omopth2  7664  swrdsbslen  13448  swrdspsleq  13449  repswswrd  13531  ramub1lem1  15730  cntzsubr  18812  lbspss  19082  maducoeval2  20446  cramer  20497  neiptopnei  20936  ptbasin  21380  basqtop  21514  tmdgsum  21899  ustuqtop1  22045  cxplea  24442  cxple2  24443  ewlkle  26501  uspgr2wlkeq2  26543  br8d  29422  isarchi2  29739  archiabllem2c  29749  cvmlift2lem10  31294  nosupbnd2lem1  31861  5segofs  32113  2llnjaN  34852  lvolnle3at  34868  paddasslem12  35117  paddasslem13  35118  atmod1i1m  35144  lhp2lt  35287  lhpexle2lem  35295  lhpmcvr3  35311  lhpat3  35332  ltrneq2  35434  trlnle  35473  trlval3  35474  trlval4  35475  cdleme0moN  35512  cdleme17b  35574  cdlemefrs29pre00  35683  cdlemefr27cl  35691  cdleme42ke  35773  cdleme42mgN  35776  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme50eq  35829  cdleme50trn3  35841  trlord  35857  cdlemg6c  35908  cdlemg11b  35930  cdlemg18a  35966  cdlemg42  36017  cdlemg46  36023  trljco  36028  tendococl  36060  cdlemj3  36111  tendotr  36118  cdlemk35s-id  36226  cdlemk39s-id  36228  cdlemk53b  36244  cdlemk53  36245  cdlemk35u  36252  tendoex  36263  cdlemm10N  36407  dihopelvalcpre  36537  dihord6apre  36545  dihord5b  36548  dihglblem5apreN  36580  dihglblem2N  36583  dihmeetlem4preN  36595  dihmeetlem6  36598  dihmeetlem10N  36605  dihmeetlem11N  36606  dihmeetlem16N  36611  dihmeetlem17N  36612  dihmeetlem18N  36613  dihmeetlem19N  36614  dihmeetALTN  36616  dihlspsnat  36622  dvh3dim2  36737  dvh3dim3N  36738  jm2.25lem1  37565  jm2.26  37569  limcperiod  39860  0ellimcdiv  39881  cncfshift  40087  cncfperiod  40092  icccncfext  40100  stoweidlem34  40251  fourierdlem48  40371  fourierdlem87  40410  sge0xaddlem2  40651  smflimsuplem7  41032  domnmsuppn0  42150