Theorem simpl1r 1226

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  soisores  7324  tfisi  7848  omopth2  8584  swrdsbslen  14614  swrdspsleq  14615  repswswrd  14734  ramub1lem1  16959  efgsfo  19607  lbspss  20693  maducoeval2  22142  madurid  22146  decpmatmullem  22273  mp2pm2mplem4  22311  llyrest  22989  ptbasin  23081  basqtop  23215  ustuqtop1  23746  mulcxp  26193  noetalem1  27244  sltmul2  27626  elwwlks2ons3im  29239  br8d  31870  isarchi2  32362  archiabllem2c  32372  cvmlift2lem10  34334  5segofs  35009  btwnconn1lem13  35102  2llnjaN  38485  paddasslem12  38750  lhp2lt  38920  lhpexle2lem  38928  lhpmcvr3  38944  lhpat3  38965  trlval3  39106  cdleme17b  39206  cdlemefr27cl  39322  cdlemg11b  39561  tendococl  39691  cdlemj3  39742  cdlemk35s-id  39857  cdlemk39s-id  39859  cdlemk53b  39875  cdlemk35u  39883  cdlemm10N  40037  dihopelvalcpre  40167  dihord6apre  40175  dihord5b  40178  dihglblem5apreN  40210  dihglblem2N  40213  dihmeetlem6  40228  dihmeetlem18N  40243  dvh3dim2  40367  dvh3dim3N  40368  jm2.25lem1  41785  limcleqr  44408  icccncfext  44651  fourierdlem87  44957  sge0seq  45210  smflimsuplem7  45590  fsupdm  45606  finfdm  45610  itscnhlc0xyqsol  47499  itscnhlinecirc02plem2  47517