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  7302  omopth2  8548  ttrcltr  9669  fin23lem11  10270  xmulasslem3  13246  ssfzo12bi  13722  ntrivcvgmul  15868  pockthg  16877  gsumsgrpccat  18767  efgred  19678  lspfixed  21038  decpmatmullem  22658  decpmatmul  22659  unconn  23316  llyrest  23372  basqtop  23598  tmdgsum  23982  tsmsxp  24042  ucncn  24172  mulcxp  26594  cxple2  26606  nogt01o  27608  noetalem1  27653  cofcut1  27828  ax5seglem1  28855  ax5seglem2  28856  axpasch  28868  axcontlem4  28894  1pthon2v  30082  mhmimasplusg  32979  cvmlift2lem10  35299  br4  35745  cgrcomim  35977  btwnintr  36007  btwnouttr2  36010  btwndiff  36015  btwnconn1lem14  36088  btwnconn3  36091  segcon2  36093  brsegle  36096  brsegle2  36097  segleantisym  36103  outsideofeu  36119  eqlkr  39092  eqlkr2  39093  lkrlsp  39095  atbtwn  39440  3dimlem3OLDN  39456  3dim3  39463  3atlem7  39483  4atlem0a  39587  4atlem3a  39591  4atlem11  39603  lneq2at  39772  lnatexN  39773  paddasslem6  39819  llnexchb2  39863  lhpexle2lem  40003  lhpexle3  40006  lhp2at0nle  40029  lhpat3  40040  trlnid  40173  ltrneq3  40202  cdleme17b  40281  cdleme27cl  40360  cdlemefrs29bpre0  40390  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdlemefs32sn1aw  40408  cdleme32le  40441  ltrniotavalbN  40578  cdlemg6  40617  cdlemg7N  40620  cdlemg11b  40636  cdlemg15a  40649  cdlemg15  40650  cdlemg39  40710  trlcone  40722  cdlemg42  40723  tendoconid  40823  tendotr  40824  cdlemk39u  40962  cdlemk19u  40964  tendoex  40969  cdlemm10N  41112  dihord2pre  41219  dihord4  41252  dihord5b  41253  dihglbcpreN  41294  dihmeetlem13N  41313  dih1dimatlem0  41322  mzpcong  42961  jm2.25lem1  42987  jm2.26  42991  idomsubgmo  43182  uhgrimisgrgric  47931  itscnhlinecirc02plem2  48772