Theorem simpl1r 1222

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 1182	1 ⊢ ((((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  soisores  7059  tfisi  7553  omopth2  8193  swrdsbslen  14017  swrdspsleq  14018  repswswrd  14137  ramub1lem1  16352  efgsfo  18857  lbspss  19847  maducoeval2  21245  madurid  21249  decpmatmullem  21376  mp2pm2mplem4  21414  llyrest  22090  ptbasin  22182  basqtop  22316  ustuqtop1  22847  mulcxp  25276  elwwlks2ons3im  27740  br8d  30374  isarchi2  30864  archiabllem2c  30874  cvmlift2lem10  32672  5segofs  33580  btwnconn1lem13  33673  2llnjaN  36862  paddasslem12  37127  lhp2lt  37297  lhpexle2lem  37305  lhpmcvr3  37321  lhpat3  37342  trlval3  37483  cdleme17b  37583  cdlemefr27cl  37699  cdlemg11b  37938  tendococl  38068  cdlemj3  38119  cdlemk35s-id  38234  cdlemk39s-id  38236  cdlemk53b  38252  cdlemk35u  38260  cdlemm10N  38414  dihopelvalcpre  38544  dihord6apre  38552  dihord5b  38555  dihglblem5apreN  38587  dihglblem2N  38590  dihmeetlem6  38605  dihmeetlem18N  38620  dvh3dim2  38744  dvh3dim3N  38745  jm2.25lem1  39939  limcleqr  42286  icccncfext  42529  fourierdlem87  42835  sge0seq  43085  smflimsuplem7  43457  itscnhlc0xyqsol  45179  itscnhlinecirc02plem2  45197