Theorem simpl2r 1227

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

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

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 1089

This theorem is referenced by:  soisores  7363  omopth2  8640  ttrcltr  9785  fin23lem11  10386  xmulasslem3  13348  ssfzo12bi  13811  ntrivcvgmul  15950  pockthg  16953  gsumsgrpccat  18875  efgred  19790  lspfixed  21153  decpmatmullem  22798  decpmatmul  22799  unconn  23458  llyrest  23514  basqtop  23740  tmdgsum  24124  tsmsxp  24184  ucncn  24315  mulcxp  26745  cxple2  26757  nogt01o  27759  noetalem1  27804  cofcut1  27972  ax5seglem1  28961  ax5seglem2  28962  axpasch  28974  axcontlem4  29000  1pthon2v  30185  mhmimasplusg  33024  cvmlift2lem10  35280  br4  35720  cgrcomim  35953  btwnintr  35983  btwnouttr2  35986  btwndiff  35991  btwnconn1lem14  36064  btwnconn3  36067  segcon2  36069  brsegle  36072  brsegle2  36073  segleantisym  36079  outsideofeu  36095  eqlkr  39055  eqlkr2  39056  lkrlsp  39058  atbtwn  39403  3dimlem3OLDN  39419  3dim3  39426  3atlem7  39446  4atlem0a  39550  4atlem3a  39554  4atlem11  39566  lneq2at  39735  lnatexN  39736  paddasslem6  39782  llnexchb2  39826  lhpexle2lem  39966  lhpexle3  39969  lhp2at0nle  39992  lhpat3  40003  trlnid  40136  ltrneq3  40165  cdleme17b  40244  cdleme27cl  40323  cdlemefrs29bpre0  40353  cdlemefrs29clN  40356  cdlemefrs32fva  40357  cdlemefs32sn1aw  40371  cdleme32le  40404  ltrniotavalbN  40541  cdlemg6  40580  cdlemg7N  40583  cdlemg11b  40599  cdlemg15a  40612  cdlemg15  40613  cdlemg39  40673  trlcone  40685  cdlemg42  40686  tendoconid  40786  tendotr  40787  cdlemk39u  40925  cdlemk19u  40927  tendoex  40932  cdlemm10N  41075  dihord2pre  41182  dihord4  41215  dihord5b  41216  dihglbcpreN  41257  dihmeetlem13N  41276  dih1dimatlem0  41285  mzpcong  42929  jm2.25lem1  42955  jm2.26  42959  idomsubgmo  43154  uhgrimisgrgric  47783  itscnhlinecirc02plem2  48517