Theorem simpl2r 1228

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 1187	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  7347  omopth2  8622  ttrcltr  9756  fin23lem11  10357  xmulasslem3  13328  ssfzo12bi  13800  ntrivcvgmul  15938  pockthg  16944  gsumsgrpccat  18853  efgred  19766  lspfixed  21130  decpmatmullem  22777  decpmatmul  22778  unconn  23437  llyrest  23493  basqtop  23719  tmdgsum  24103  tsmsxp  24163  ucncn  24294  mulcxp  26727  cxple2  26739  nogt01o  27741  noetalem1  27786  cofcut1  27954  ax5seglem1  28943  ax5seglem2  28944  axpasch  28956  axcontlem4  28982  1pthon2v  30172  mhmimasplusg  33043  cvmlift2lem10  35317  br4  35758  cgrcomim  35990  btwnintr  36020  btwnouttr2  36023  btwndiff  36028  btwnconn1lem14  36101  btwnconn3  36104  segcon2  36106  brsegle  36109  brsegle2  36110  segleantisym  36116  outsideofeu  36132  eqlkr  39100  eqlkr2  39101  lkrlsp  39103  atbtwn  39448  3dimlem3OLDN  39464  3dim3  39471  3atlem7  39491  4atlem0a  39595  4atlem3a  39599  4atlem11  39611  lneq2at  39780  lnatexN  39781  paddasslem6  39827  llnexchb2  39871  lhpexle2lem  40011  lhpexle3  40014  lhp2at0nle  40037  lhpat3  40048  trlnid  40181  ltrneq3  40210  cdleme17b  40289  cdleme27cl  40368  cdlemefrs29bpre0  40398  cdlemefrs29clN  40401  cdlemefrs32fva  40402  cdlemefs32sn1aw  40416  cdleme32le  40449  ltrniotavalbN  40586  cdlemg6  40625  cdlemg7N  40628  cdlemg11b  40644  cdlemg15a  40657  cdlemg15  40658  cdlemg39  40718  trlcone  40730  cdlemg42  40731  tendoconid  40831  tendotr  40832  cdlemk39u  40970  cdlemk19u  40972  tendoex  40977  cdlemm10N  41120  dihord2pre  41227  dihord4  41260  dihord5b  41261  dihglbcpreN  41302  dihmeetlem13N  41321  dih1dimatlem0  41330  mzpcong  42984  jm2.25lem1  43010  jm2.26  43014  idomsubgmo  43205  uhgrimisgrgric  47899  itscnhlinecirc02plem2  48704