Theorem simpl2r 1244

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 780	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜓)
2	1	3ad2antl2 1203	1 ⊢ (((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  soisores  7315  omopth2  8557  ttrcltr  9673  fin23lem11  10289  xmulasslem3  13303  ssfzo12bi  13781  ntrivcvgmul  15946  pockthg  16956  gsumsgrpccat  18889  efgred  19809  lspfixed  21221  decpmatmullem  22889  decpmatmul  22890  unconn  23547  llyrest  23603  basqtop  23829  tmdgsum  24213  tsmsxp  24273  ucncn  24402  mulcxp  26808  cxple2  26820  nogt01o  27818  noetalem1  27863  cofcut1  28071  bdayfinbndlem1  28618  ax5seglem1  29187  ax5seglem2  29188  axpasch  29200  axcontlem4  29226  1pthon2v  30413  mhmimasplusg  33270  cvmlift2lem10  35675  br4  36121  cgrcomim  36352  btwnintr  36382  btwnouttr2  36385  btwndiff  36390  btwnconn1lem14  36463  btwnconn3  36466  segcon2  36468  brsegle  36471  brsegle2  36472  segleantisym  36478  outsideofeu  36494  eqlkr  39735  eqlkr2  39736  lkrlsp  39738  atbtwn  40082  3dimlem3OLDN  40098  3dim3  40105  3atlem7  40125  4atlem0a  40229  4atlem3a  40233  4atlem11  40245  lneq2at  40414  lnatexN  40415  paddasslem6  40461  llnexchb2  40505  lhpexle2lem  40645  lhpexle3  40648  lhp2at0nle  40671  lhpat3  40682  trlnid  40815  ltrneq3  40844  cdleme17b  40923  cdleme27cl  41002  cdlemefrs29bpre0  41032  cdlemefrs29clN  41035  cdlemefrs32fva  41036  cdlemefs32sn1aw  41050  cdleme32le  41083  ltrniotavalbN  41220  cdlemg6  41259  cdlemg7N  41262  cdlemg11b  41278  cdlemg15a  41291  cdlemg15  41292  cdlemg39  41352  trlcone  41364  cdlemg42  41365  tendoconid  41465  tendotr  41466  cdlemk39u  41604  cdlemk19u  41606  tendoex  41611  cdlemm10N  41754  dihord2pre  41861  dihord4  41894  dihord5b  41895  dihglbcpreN  41936  dihmeetlem13N  41955  dih1dimatlem0  41964  mzpcong  43561  jm2.25lem1  43587  jm2.26  43591  idomsubgmo  43782  uhgrimisgrgric  48551  itscnhlinecirc02plem2  49414