Theorem simpl2r 1246

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  soisores  7332  omopth2  8575  ttrcltr  9699  fin23lem11  10323  xmulasslem3  13342  ssfzo12bi  13821  ntrivcvgmul  15995  pockthg  17004  gsumsgrpccat  18955  efgred  19881  lspfixed  21321  decpmatmullem  23002  decpmatmul  23003  unconn  23660  llyrest  23717  basqtop  23943  tmdgsum  24327  tsmsxp  24387  ucncn  24516  mulcxp  26930  cxple2  26942  nogt01o  27940  noetalem1  27985  cofcut1  28193  bdayfinbndlem1  28740  ax5seglem1  29393  ax5seglem2  29394  axpasch  29406  axcontlem4  29432  1pthon2v  30641  mhmimasplusg  33485  cvmlift2lem10  35899  br4  36345  cgrcomim  36577  btwnintr  36607  btwnouttr2  36610  btwndiff  36615  btwnconn1lem14  36688  btwnconn3  36691  segcon2  36693  brsegle  36696  brsegle2  36697  segleantisym  36703  outsideofeu  36719  eqlkr  39980  eqlkr2  39981  lkrlsp  39983  atbtwn  40327  3dimlem3OLDN  40343  3dim3  40350  3atlem7  40370  4atlem0a  40474  4atlem3a  40478  4atlem11  40490  lneq2at  40659  lnatexN  40660  paddasslem6  40706  llnexchb2  40750  lhpexle2lem  40890  lhpexle3  40893  lhp2at0nle  40916  lhpat3  40927  trlnid  41060  ltrneq3  41089  cdleme17b  41168  cdleme27cl  41247  cdlemefrs29bpre0  41277  cdlemefrs29clN  41280  cdlemefrs32fva  41281  cdlemefs32sn1aw  41295  cdleme32le  41328  ltrniotavalbN  41465  cdlemg6  41504  cdlemg7N  41507  cdlemg11b  41523  cdlemg15a  41536  cdlemg15  41537  cdlemg39  41597  trlcone  41609  cdlemg42  41610  tendoconid  41710  tendotr  41711  cdlemk39u  41849  cdlemk19u  41851  tendoex  41856  cdlemm10N  41999  dihord2pre  42106  dihord4  42139  dihord5b  42140  dihglbcpreN  42181  dihmeetlem13N  42200  dih1dimatlem0  42209  mzpcong  43821  jm2.25lem1  43847  jm2.26  43851  idomsubgmo  44042  uhgrimisgrgric  48855  itscnhlinecirc02plem2  49721