Theorem simpl2r 1223

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

Assertion

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

Proof of Theorem simpl2r

Step	Hyp	Ref	Expression
1		simplr 767	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1182	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  soisores  7080  omopth2  8210  fin23lem11  9739  xmulasslem3  12680  ssfzo12bi  13133  ntrivcvgmul  15258  pockthg  16242  gsumsgrpccat  18004  efgred  18874  lspfixed  19900  decpmatmullem  21379  decpmatmul  21380  unconn  22037  llyrest  22093  basqtop  22319  tmdgsum  22703  tsmsxp  22763  ucncn  22894  mulcxp  25268  cxple2  25280  ax5seglem1  26714  ax5seglem2  26715  axpasch  26727  axcontlem4  26753  1pthon2v  27932  cvmlift2lem10  32559  br4  32994  cgrcomim  33450  btwnintr  33480  btwnouttr2  33483  btwndiff  33488  btwnconn1lem14  33561  btwnconn3  33564  segcon2  33566  brsegle  33569  brsegle2  33570  segleantisym  33576  outsideofeu  33592  eqlkr  36250  eqlkr2  36251  lkrlsp  36253  atbtwn  36597  3dimlem3OLDN  36613  3dim3  36620  3atlem7  36640  4atlem0a  36744  4atlem3a  36748  4atlem11  36760  lneq2at  36929  lnatexN  36930  paddasslem6  36976  llnexchb2  37020  lhpexle2lem  37160  lhpexle3  37163  lhp2at0nle  37186  lhpat3  37197  trlnid  37330  ltrneq3  37359  cdleme17b  37438  cdleme27cl  37517  cdlemefrs29bpre0  37547  cdlemefrs29clN  37550  cdlemefrs32fva  37551  cdlemefs32sn1aw  37565  cdleme32le  37598  ltrniotavalbN  37735  cdlemg6  37774  cdlemg7N  37777  cdlemg11b  37793  cdlemg15a  37806  cdlemg15  37807  cdlemg39  37867  trlcone  37879  cdlemg42  37880  tendoconid  37980  tendotr  37981  cdlemk39u  38119  cdlemk19u  38121  tendoex  38126  cdlemm10N  38269  dihord2pre  38376  dihord4  38409  dihord5b  38410  dihglbcpreN  38451  dihmeetlem13N  38470  dih1dimatlem0  38479  mzpcong  39589  jm2.25lem1  39615  jm2.26  39619  idomsubgmo  39818  itscnhlinecirc02plem2  44790