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 768	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1187	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  7267  omopth2  8505  ttrcltr  9613  fin23lem11  10215  xmulasslem3  13187  ssfzo12bi  13663  ntrivcvgmul  15811  pockthg  16820  gsumsgrpccat  18750  efgred  19662  lspfixed  21067  decpmatmullem  22687  decpmatmul  22688  unconn  23345  llyrest  23401  basqtop  23627  tmdgsum  24011  tsmsxp  24071  ucncn  24200  mulcxp  26622  cxple2  26634  nogt01o  27636  noetalem1  27681  cofcut1  27865  ax5seglem1  28908  ax5seglem2  28909  axpasch  28921  axcontlem4  28947  1pthon2v  30135  mhmimasplusg  33026  cvmlift2lem10  35377  br4  35823  cgrcomim  36054  btwnintr  36084  btwnouttr2  36087  btwndiff  36092  btwnconn1lem14  36165  btwnconn3  36168  segcon2  36170  brsegle  36173  brsegle2  36174  segleantisym  36180  outsideofeu  36196  eqlkr  39218  eqlkr2  39219  lkrlsp  39221  atbtwn  39565  3dimlem3OLDN  39581  3dim3  39588  3atlem7  39608  4atlem0a  39712  4atlem3a  39716  4atlem11  39728  lneq2at  39897  lnatexN  39898  paddasslem6  39944  llnexchb2  39988  lhpexle2lem  40128  lhpexle3  40131  lhp2at0nle  40154  lhpat3  40165  trlnid  40298  ltrneq3  40327  cdleme17b  40406  cdleme27cl  40485  cdlemefrs29bpre0  40515  cdlemefrs29clN  40518  cdlemefrs32fva  40519  cdlemefs32sn1aw  40533  cdleme32le  40566  ltrniotavalbN  40703  cdlemg6  40742  cdlemg7N  40745  cdlemg11b  40761  cdlemg15a  40774  cdlemg15  40775  cdlemg39  40835  trlcone  40847  cdlemg42  40848  tendoconid  40948  tendotr  40949  cdlemk39u  41087  cdlemk19u  41089  tendoex  41094  cdlemm10N  41237  dihord2pre  41344  dihord4  41377  dihord5b  41378  dihglbcpreN  41419  dihmeetlem13N  41438  dih1dimatlem0  41447  mzpcong  43089  jm2.25lem1  43115  jm2.26  43119  idomsubgmo  43310  uhgrimisgrgric  48055  itscnhlinecirc02plem2  48908