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  7268  omopth2  8509  ttrcltr  9631  fin23lem11  10230  xmulasslem3  13206  ssfzo12bi  13682  ntrivcvgmul  15827  pockthg  16836  gsumsgrpccat  18732  efgred  19645  lspfixed  21053  decpmatmullem  22674  decpmatmul  22675  unconn  23332  llyrest  23388  basqtop  23614  tmdgsum  23998  tsmsxp  24058  ucncn  24188  mulcxp  26610  cxple2  26622  nogt01o  27624  noetalem1  27669  cofcut1  27851  ax5seglem1  28891  ax5seglem2  28892  axpasch  28904  axcontlem4  28930  1pthon2v  30115  mhmimasplusg  33005  cvmlift2lem10  35284  br4  35730  cgrcomim  35962  btwnintr  35992  btwnouttr2  35995  btwndiff  36000  btwnconn1lem14  36073  btwnconn3  36076  segcon2  36078  brsegle  36081  brsegle2  36082  segleantisym  36088  outsideofeu  36104  eqlkr  39077  eqlkr2  39078  lkrlsp  39080  atbtwn  39425  3dimlem3OLDN  39441  3dim3  39448  3atlem7  39468  4atlem0a  39572  4atlem3a  39576  4atlem11  39588  lneq2at  39757  lnatexN  39758  paddasslem6  39804  llnexchb2  39848  lhpexle2lem  39988  lhpexle3  39991  lhp2at0nle  40014  lhpat3  40025  trlnid  40158  ltrneq3  40187  cdleme17b  40266  cdleme27cl  40345  cdlemefrs29bpre0  40375  cdlemefrs29clN  40378  cdlemefrs32fva  40379  cdlemefs32sn1aw  40393  cdleme32le  40426  ltrniotavalbN  40563  cdlemg6  40602  cdlemg7N  40605  cdlemg11b  40621  cdlemg15a  40634  cdlemg15  40635  cdlemg39  40695  trlcone  40707  cdlemg42  40708  tendoconid  40808  tendotr  40809  cdlemk39u  40947  cdlemk19u  40949  tendoex  40954  cdlemm10N  41097  dihord2pre  41204  dihord4  41237  dihord5b  41238  dihglbcpreN  41279  dihmeetlem13N  41298  dih1dimatlem0  41307  mzpcong  42945  jm2.25lem1  42971  jm2.26  42975  idomsubgmo  43166  uhgrimisgrgric  47916  itscnhlinecirc02plem2  48769