Theorem simpl1r 1244

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

Assertion

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

Proof of Theorem simpl1r

Step	Hyp	Ref	Expression
1		simplr 781	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl1 1204	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7335  tfisi  7870  omopth2  8595  swrdsbslen  14818  swrdspsleq  14819  repswswrd  14939  ramub1lem1  17209  efgsfo  19958  lbspss  21362  maducoeval2  22960  madurid  22964  decpmatmullem  23094  mp2pm2mplem4  23132  llyrest  23809  ptbasin  23901  basqtop  24035  ustuqtop1  24565  mulcxp  27018  noetalem1  28103  ltmuls2  28562  elwwlks2ons3im  30548  br8d  33249  isarchi2  33792  archiabllem2c  33802  cvmlift2lem10  36163  5segofs  36863  btwnconn1lem13  36956  2llnjaN  40716  paddasslem12  40981  lhp2lt  41151  lhpexle2lem  41159  lhpmcvr3  41175  lhpat3  41196  trlval3  41337  cdleme17b  41437  cdlemefr27cl  41553  cdlemg11b  41792  tendococl  41922  cdlemj3  41973  cdlemk35s-id  42088  cdlemk39s-id  42090  cdlemk53b  42106  cdlemk35u  42114  cdlemm10N  42268  dihopelvalcpre  42398  dihord6apre  42406  dihord5b  42409  dihglblem5apreN  42441  dihglblem2N  42444  dihmeetlem6  42459  dihmeetlem18N  42474  dvh3dim2  42598  dvh3dim3N  42599  jm2.25lem1  44098  limcleqr  46747  icccncfext  46990  fourierdlem87  47296  sge0seq  47549  smflimsuplem7  47929  fsupdm  47945  finfdm  47949  itscnhlc0xyqsol  49970  itscnhlinecirc02plem2  49988