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  27623  elwwlks2ons3im  29208  br8d  31839  isarchi2  32331  archiabllem2c  32341  cvmlift2lem10  34303  5segofs  34978  btwnconn1lem13  35071  2llnjaN  38437  paddasslem12  38702  lhp2lt  38872  lhpexle2lem  38880  lhpmcvr3  38896  lhpat3  38917  trlval3  39058  cdleme17b  39158  cdlemefr27cl  39274  cdlemg11b  39513  tendococl  39643  cdlemj3  39694  cdlemk35s-id  39809  cdlemk39s-id  39811  cdlemk53b  39827  cdlemk35u  39835  cdlemm10N  39989  dihopelvalcpre  40119  dihord6apre  40127  dihord5b  40130  dihglblem5apreN  40162  dihglblem2N  40165  dihmeetlem6  40180  dihmeetlem18N  40195  dvh3dim2  40319  dvh3dim3N  40320  jm2.25lem1  41737  limcleqr  44360  icccncfext  44603  fourierdlem87  44909  sge0seq  45162  smflimsuplem7  45542  fsupdm  45558  finfdm  45562  itscnhlc0xyqsol  47451  itscnhlinecirc02plem2  47469