Theorem simpl2r 1226

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

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

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

This theorem is referenced by:  soisores  7347  omopth2  8621  ttrcltr  9754  fin23lem11  10355  xmulasslem3  13325  ssfzo12bi  13797  ntrivcvgmul  15935  pockthg  16940  gsumsgrpccat  18866  efgred  19781  lspfixed  21148  decpmatmullem  22793  decpmatmul  22794  unconn  23453  llyrest  23509  basqtop  23735  tmdgsum  24119  tsmsxp  24179  ucncn  24310  mulcxp  26742  cxple2  26754  nogt01o  27756  noetalem1  27801  cofcut1  27969  ax5seglem1  28958  ax5seglem2  28959  axpasch  28971  axcontlem4  28997  1pthon2v  30182  mhmimasplusg  33026  cvmlift2lem10  35297  br4  35738  cgrcomim  35971  btwnintr  36001  btwnouttr2  36004  btwndiff  36009  btwnconn1lem14  36082  btwnconn3  36085  segcon2  36087  brsegle  36090  brsegle2  36091  segleantisym  36097  outsideofeu  36113  eqlkr  39081  eqlkr2  39082  lkrlsp  39084  atbtwn  39429  3dimlem3OLDN  39445  3dim3  39452  3atlem7  39472  4atlem0a  39576  4atlem3a  39580  4atlem11  39592  lneq2at  39761  lnatexN  39762  paddasslem6  39808  llnexchb2  39852  lhpexle2lem  39992  lhpexle3  39995  lhp2at0nle  40018  lhpat3  40029  trlnid  40162  ltrneq3  40191  cdleme17b  40270  cdleme27cl  40349  cdlemefrs29bpre0  40379  cdlemefrs29clN  40382  cdlemefrs32fva  40383  cdlemefs32sn1aw  40397  cdleme32le  40430  ltrniotavalbN  40567  cdlemg6  40606  cdlemg7N  40609  cdlemg11b  40625  cdlemg15a  40638  cdlemg15  40639  cdlemg39  40699  trlcone  40711  cdlemg42  40712  tendoconid  40812  tendotr  40813  cdlemk39u  40951  cdlemk19u  40953  tendoex  40958  cdlemm10N  41101  dihord2pre  41208  dihord4  41241  dihord5b  41242  dihglbcpreN  41283  dihmeetlem13N  41302  dih1dimatlem0  41311  mzpcong  42961  jm2.25lem1  42987  jm2.26  42991  idomsubgmo  43182  uhgrimisgrgric  47837  itscnhlinecirc02plem2  48633