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  7282  omopth2  8519  ttrcltr  9637  fin23lem11  10239  xmulasslem3  13238  ssfzo12bi  13716  ntrivcvgmul  15867  pockthg  16877  gsumsgrpccat  18808  efgred  19723  lspfixed  21126  decpmatmullem  22736  decpmatmul  22737  unconn  23394  llyrest  23450  basqtop  23676  tmdgsum  24060  tsmsxp  24120  ucncn  24249  mulcxp  26649  cxple2  26661  nogt01o  27660  noetalem1  27705  cofcut1  27912  bdayfinbndlem1  28459  ax5seglem1  28997  ax5seglem2  28998  axpasch  29010  axcontlem4  29036  1pthon2v  30223  mhmimasplusg  33098  cvmlift2lem10  35494  br4  35940  cgrcomim  36171  btwnintr  36201  btwnouttr2  36204  btwndiff  36209  btwnconn1lem14  36282  btwnconn3  36285  segcon2  36287  brsegle  36290  brsegle2  36291  segleantisym  36297  outsideofeu  36313  eqlkr  39545  eqlkr2  39546  lkrlsp  39548  atbtwn  39892  3dimlem3OLDN  39908  3dim3  39915  3atlem7  39935  4atlem0a  40039  4atlem3a  40043  4atlem11  40055  lneq2at  40224  lnatexN  40225  paddasslem6  40271  llnexchb2  40315  lhpexle2lem  40455  lhpexle3  40458  lhp2at0nle  40481  lhpat3  40492  trlnid  40625  ltrneq3  40654  cdleme17b  40733  cdleme27cl  40812  cdlemefrs29bpre0  40842  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdlemefs32sn1aw  40860  cdleme32le  40893  ltrniotavalbN  41030  cdlemg6  41069  cdlemg7N  41072  cdlemg11b  41088  cdlemg15a  41101  cdlemg15  41102  cdlemg39  41162  trlcone  41174  cdlemg42  41175  tendoconid  41275  tendotr  41276  cdlemk39u  41414  cdlemk19u  41416  tendoex  41421  cdlemm10N  41564  dihord2pre  41671  dihord4  41704  dihord5b  41705  dihglbcpreN  41746  dihmeetlem13N  41765  dih1dimatlem0  41774  mzpcong  43400  jm2.25lem1  43426  jm2.26  43430  idomsubgmo  43621  uhgrimisgrgric  48407  itscnhlinecirc02plem2  49259