Theorem simpl2r 1225

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 765	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1184	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  soisores  7178  omopth2  8377  fin23lem11  10004  xmulasslem3  12949  ssfzo12bi  13410  ntrivcvgmul  15542  pockthg  16535  gsumsgrpccat  18393  efgred  19269  lspfixed  20305  decpmatmullem  21828  decpmatmul  21829  unconn  22488  llyrest  22544  basqtop  22770  tmdgsum  23154  tsmsxp  23214  ucncn  23345  mulcxp  25745  cxple2  25757  ax5seglem1  27199  ax5seglem2  27200  axpasch  27212  axcontlem4  27238  1pthon2v  28418  cvmlift2lem10  33174  br4  33631  ttrcltr  33702  nogt01o  33826  noetalem1  33871  cofcut1  34017  cgrcomim  34218  btwnintr  34248  btwnouttr2  34251  btwndiff  34256  btwnconn1lem14  34329  btwnconn3  34332  segcon2  34334  brsegle  34337  brsegle2  34338  segleantisym  34344  outsideofeu  34360  eqlkr  37040  eqlkr2  37041  lkrlsp  37043  atbtwn  37387  3dimlem3OLDN  37403  3dim3  37410  3atlem7  37430  4atlem0a  37534  4atlem3a  37538  4atlem11  37550  lneq2at  37719  lnatexN  37720  paddasslem6  37766  llnexchb2  37810  lhpexle2lem  37950  lhpexle3  37953  lhp2at0nle  37976  lhpat3  37987  trlnid  38120  ltrneq3  38149  cdleme17b  38228  cdleme27cl  38307  cdlemefrs29bpre0  38337  cdlemefrs29clN  38340  cdlemefrs32fva  38341  cdlemefs32sn1aw  38355  cdleme32le  38388  ltrniotavalbN  38525  cdlemg6  38564  cdlemg7N  38567  cdlemg11b  38583  cdlemg15a  38596  cdlemg15  38597  cdlemg39  38657  trlcone  38669  cdlemg42  38670  tendoconid  38770  tendotr  38771  cdlemk39u  38909  cdlemk19u  38911  tendoex  38916  cdlemm10N  39059  dihord2pre  39166  dihord4  39199  dihord5b  39200  dihglbcpreN  39241  dihmeetlem13N  39260  dih1dimatlem0  39269  mzpcong  40710  jm2.25lem1  40736  jm2.26  40740  idomsubgmo  40939  itscnhlinecirc02plem2  46017