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 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  soisores  7114  omopth2  8290  fin23lem11  9896  xmulasslem3  12841  ssfzo12bi  13302  ntrivcvgmul  15429  pockthg  16422  gsumsgrpccat  18220  efgred  19092  lspfixed  20119  decpmatmullem  21622  decpmatmul  21623  unconn  22280  llyrest  22336  basqtop  22562  tmdgsum  22946  tsmsxp  23006  ucncn  23136  mulcxp  25527  cxple2  25539  ax5seglem1  26973  ax5seglem2  26974  axpasch  26986  axcontlem4  27012  1pthon2v  28190  cvmlift2lem10  32941  br4  33395  nogt01o  33585  noetalem1  33630  cofcut1  33776  cgrcomim  33977  btwnintr  34007  btwnouttr2  34010  btwndiff  34015  btwnconn1lem14  34088  btwnconn3  34091  segcon2  34093  brsegle  34096  brsegle2  34097  segleantisym  34103  outsideofeu  34119  eqlkr  36799  eqlkr2  36800  lkrlsp  36802  atbtwn  37146  3dimlem3OLDN  37162  3dim3  37169  3atlem7  37189  4atlem0a  37293  4atlem3a  37297  4atlem11  37309  lneq2at  37478  lnatexN  37479  paddasslem6  37525  llnexchb2  37569  lhpexle2lem  37709  lhpexle3  37712  lhp2at0nle  37735  lhpat3  37746  trlnid  37879  ltrneq3  37908  cdleme17b  37987  cdleme27cl  38066  cdlemefrs29bpre0  38096  cdlemefrs29clN  38099  cdlemefrs32fva  38100  cdlemefs32sn1aw  38114  cdleme32le  38147  ltrniotavalbN  38284  cdlemg6  38323  cdlemg7N  38326  cdlemg11b  38342  cdlemg15a  38355  cdlemg15  38356  cdlemg39  38416  trlcone  38428  cdlemg42  38429  tendoconid  38529  tendotr  38530  cdlemk39u  38668  cdlemk19u  38670  tendoex  38675  cdlemm10N  38818  dihord2pre  38925  dihord4  38958  dihord5b  38959  dihglbcpreN  39000  dihmeetlem13N  39019  dih1dimatlem0  39028  mzpcong  40438  jm2.25lem1  40464  jm2.26  40468  idomsubgmo  40667  itscnhlinecirc02plem2  45745