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 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  soisores  7273  omopth2  8510  ttrcltr  9626  fin23lem11  10228  xmulasslem3  13227  ssfzo12bi  13705  ntrivcvgmul  15856  pockthg  16866  gsumsgrpccat  18797  efgred  19712  lspfixed  21116  decpmatmullem  22745  decpmatmul  22746  unconn  23403  llyrest  23459  basqtop  23685  tmdgsum  24069  tsmsxp  24129  ucncn  24258  mulcxp  26665  cxple2  26677  nogt01o  27679  noetalem1  27724  cofcut1  27931  bdayfinbndlem1  28478  ax5seglem1  29016  ax5seglem2  29017  axpasch  29029  axcontlem4  29055  1pthon2v  30243  mhmimasplusg  33118  cvmlift2lem10  35515  br4  35961  cgrcomim  36192  btwnintr  36222  btwnouttr2  36225  btwndiff  36230  btwnconn1lem14  36303  btwnconn3  36306  segcon2  36308  brsegle  36311  brsegle2  36312  segleantisym  36318  outsideofeu  36334  eqlkr  39556  eqlkr2  39557  lkrlsp  39559  atbtwn  39903  3dimlem3OLDN  39919  3dim3  39926  3atlem7  39946  4atlem0a  40050  4atlem3a  40054  4atlem11  40066  lneq2at  40235  lnatexN  40236  paddasslem6  40282  llnexchb2  40326  lhpexle2lem  40466  lhpexle3  40469  lhp2at0nle  40492  lhpat3  40503  trlnid  40636  ltrneq3  40665  cdleme17b  40744  cdleme27cl  40823  cdlemefrs29bpre0  40853  cdlemefrs29clN  40856  cdlemefrs32fva  40857  cdlemefs32sn1aw  40871  cdleme32le  40904  ltrniotavalbN  41041  cdlemg6  41080  cdlemg7N  41083  cdlemg11b  41099  cdlemg15a  41112  cdlemg15  41113  cdlemg39  41173  trlcone  41185  cdlemg42  41186  tendoconid  41286  tendotr  41287  cdlemk39u  41425  cdlemk19u  41427  tendoex  41432  cdlemm10N  41575  dihord2pre  41682  dihord4  41715  dihord5b  41716  dihglbcpreN  41757  dihmeetlem13N  41776  dih1dimatlem0  41785  mzpcong  43415  jm2.25lem1  43441  jm2.26  43445  idomsubgmo  43636  uhgrimisgrgric  48404  itscnhlinecirc02plem2  49256