Theorem simpl2r 1229

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 1188	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  7283  omopth2  8521  ttrcltr  9637  fin23lem11  10239  xmulasslem3  13213  ssfzo12bi  13689  ntrivcvgmul  15837  pockthg  16846  gsumsgrpccat  18777  efgred  19689  lspfixed  21095  decpmatmullem  22727  decpmatmul  22728  unconn  23385  llyrest  23441  basqtop  23667  tmdgsum  24051  tsmsxp  24111  ucncn  24240  mulcxp  26662  cxple2  26674  nogt01o  27676  noetalem1  27721  cofcut1  27928  bdayfinbndlem1  28475  ax5seglem1  29013  ax5seglem2  29014  axpasch  29026  axcontlem4  29052  1pthon2v  30240  mhmimasplusg  33130  cvmlift2lem10  35525  br4  35971  cgrcomim  36202  btwnintr  36232  btwnouttr2  36235  btwndiff  36240  btwnconn1lem14  36313  btwnconn3  36316  segcon2  36318  brsegle  36321  brsegle2  36322  segleantisym  36328  outsideofeu  36344  eqlkr  39469  eqlkr2  39470  lkrlsp  39472  atbtwn  39816  3dimlem3OLDN  39832  3dim3  39839  3atlem7  39859  4atlem0a  39963  4atlem3a  39967  4atlem11  39979  lneq2at  40148  lnatexN  40149  paddasslem6  40195  llnexchb2  40239  lhpexle2lem  40379  lhpexle3  40382  lhp2at0nle  40405  lhpat3  40416  trlnid  40549  ltrneq3  40578  cdleme17b  40657  cdleme27cl  40736  cdlemefrs29bpre0  40766  cdlemefrs29clN  40769  cdlemefrs32fva  40770  cdlemefs32sn1aw  40784  cdleme32le  40817  ltrniotavalbN  40954  cdlemg6  40993  cdlemg7N  40996  cdlemg11b  41012  cdlemg15a  41025  cdlemg15  41026  cdlemg39  41086  trlcone  41098  cdlemg42  41099  tendoconid  41199  tendotr  41200  cdlemk39u  41338  cdlemk19u  41340  tendoex  41345  cdlemm10N  41488  dihord2pre  41595  dihord4  41628  dihord5b  41629  dihglbcpreN  41670  dihmeetlem13N  41689  dih1dimatlem0  41698  mzpcong  43323  jm2.25lem1  43349  jm2.26  43353  idomsubgmo  43544  uhgrimisgrgric  48285  itscnhlinecirc02plem2  49137