Theorem simpl1l 1105

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

Assertion

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

Proof of Theorem simpl1l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  soisores  6477  tfisi  6950  omopth2  7551  swrdsbslen  13300  swrdspsleq  13301  repswswrd  13382  ramub1lem1  15568  cntzsubr  18635  lbspss  18903  maducoeval2  20265  cramer  20316  neiptopnei  20746  ptbasin  21190  basqtop  21324  tmdgsum  21709  ustuqtop1  21855  cxplea  24242  cxple2  24243  usg2wlkeq2  26237  br8d  28802  isarchi2  29070  archiabllem2c  29080  cvmlift2lem10  30548  5segofs  31283  2llnjaN  33870  lvolnle3at  33886  paddasslem12  34135  paddasslem13  34136  atmod1i1m  34162  lhp2lt  34305  lhpexle2lem  34313  lhpmcvr3  34329  lhpat3  34350  ltrneq2  34452  trlnle  34491  trlval3  34492  trlval4  34493  cdleme0moN  34530  cdleme17b  34592  cdlemefrs29pre00  34701  cdlemefr27cl  34709  cdleme42ke  34791  cdleme42mgN  34794  cdleme46f2g2  34799  cdleme46f2g1  34800  cdleme50eq  34847  cdleme50trn3  34859  trlord  34875  cdlemg6c  34926  cdlemg11b  34948  cdlemg18a  34984  cdlemg42  35035  cdlemg46  35041  trljco  35046  tendococl  35078  cdlemj3  35129  tendotr  35136  cdlemk35s-id  35244  cdlemk39s-id  35246  cdlemk53b  35262  cdlemk53  35263  cdlemk35u  35270  tendoex  35281  cdlemm10N  35425  dihopelvalcpre  35555  dihord6apre  35563  dihord5b  35566  dihglblem5apreN  35598  dihglblem2N  35601  dihmeetlem4preN  35613  dihmeetlem6  35616  dihmeetlem10N  35623  dihmeetlem11N  35624  dihmeetlem16N  35629  dihmeetlem17N  35630  dihmeetlem18N  35631  dihmeetlem19N  35632  dihmeetALTN  35634  dihlspsnat  35640  dvh3dim2  35755  dvh3dim3N  35756  jm2.25lem1  36583  jm2.26  36587  limcperiod  38695  0ellimcdiv  38716  cncfshift  38759  cncfperiod  38764  icccncfext  38773  stoweidlem34  38927  fourierdlem48  39047  fourierdlem87  39086  sge0xaddlem2  39327  ewlkle  40807  uspgr2wlkeq2  40855  av-extwwlkfablem2  41510  domnmsuppn0  41944