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  7336  omopth2  8578  ttrcltr  9695  fin23lem11  10319  xmulasslem3  13330  ssfzo12bi  13809  ntrivcvgmul  15982  pockthg  16991  gsumsgrpccat  18930  efgred  19849  lspfixed  21289  decpmatmullem  22965  decpmatmul  22966  unconn  23623  llyrest  23679  basqtop  23905  tmdgsum  24289  tsmsxp  24349  ucncn  24478  mulcxp  26887  cxple2  26899  nogt01o  27897  noetalem1  27942  cofcut1  28150  bdayfinbndlem1  28697  ax5seglem1  29315  ax5seglem2  29316  axpasch  29328  axcontlem4  29354  1pthon2v  30541  mhmimasplusg  33388  cvmlift2lem10  35825  br4  36271  cgrcomim  36502  btwnintr  36532  btwnouttr2  36535  btwndiff  36540  btwnconn1lem14  36613  btwnconn3  36616  segcon2  36618  brsegle  36621  brsegle2  36622  segleantisym  36628  outsideofeu  36644  eqlkr  39914  eqlkr2  39915  lkrlsp  39917  atbtwn  40261  3dimlem3OLDN  40277  3dim3  40284  3atlem7  40304  4atlem0a  40408  4atlem3a  40412  4atlem11  40424  lneq2at  40593  lnatexN  40594  paddasslem6  40640  llnexchb2  40684  lhpexle2lem  40824  lhpexle3  40827  lhp2at0nle  40850  lhpat3  40861  trlnid  40994  ltrneq3  41023  cdleme17b  41102  cdleme27cl  41181  cdlemefrs29bpre0  41211  cdlemefrs29clN  41214  cdlemefrs32fva  41215  cdlemefs32sn1aw  41229  cdleme32le  41262  ltrniotavalbN  41399  cdlemg6  41438  cdlemg7N  41441  cdlemg11b  41457  cdlemg15a  41470  cdlemg15  41471  cdlemg39  41531  trlcone  41543  cdlemg42  41544  tendoconid  41644  tendotr  41645  cdlemk39u  41783  cdlemk19u  41785  tendoex  41790  cdlemm10N  41933  dihord2pre  42040  dihord4  42073  dihord5b  42074  dihglbcpreN  42115  dihmeetlem13N  42134  dih1dimatlem0  42143  mzpcong  43740  jm2.25lem1  43766  jm2.26  43770  idomsubgmo  43961  uhgrimisgrgric  48737  itscnhlinecirc02plem2  49604