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  7361  omopth2  8623  ttrcltr  9747  fin23lem11  10425  xmulasslem3  13446  ssfzo12bi  13926  ntrivcvgmul  16103  pockthg  17116  gsumsgrpccat  19068  efgred  19995  lspfixed  21439  decpmatmullem  23122  decpmatmul  23123  unconn  23780  llyrest  23837  basqtop  24063  tmdgsum  24447  tsmsxp  24507  ucncn  24636  mulcxp  27046  cxple2  27058  nogt01o  28086  noetalem1  28131  cofcut1  28339  bdayfinbndlem1  28886  ax5seglem1  29539  ax5seglem2  29540  axpasch  29552  axcontlem4  29578  1pthon2v  30787  mhmimasplusg  33674  cvmlift2lem10  36257  br4  36714  cgrcomim  36945  btwnintr  36975  btwnouttr2  36978  btwndiff  36983  btwnconn1lem14  37056  btwnconn3  37059  segcon2  37061  brsegle  37064  brsegle2  37065  segleantisym  37071  outsideofeu  37087  eqlkr  40359  eqlkr2  40360  lkrlsp  40362  atbtwn  40706  3dimlem3OLDN  40722  3dim3  40729  3atlem7  40749  4atlem0a  40853  4atlem3a  40857  4atlem11  40869  lneq2at  41038  lnatexN  41039  paddasslem6  41085  llnexchb2  41129  lhpexle2lem  41269  lhpexle3  41272  lhp2at0nle  41295  lhpat3  41306  trlnid  41439  ltrneq3  41468  cdleme17b  41547  cdleme27cl  41626  cdlemefrs29bpre0  41656  cdlemefrs29clN  41659  cdlemefrs32fva  41660  cdlemefs32sn1aw  41674  cdleme32le  41707  ltrniotavalbN  41844  cdlemg6  41883  cdlemg7N  41886  cdlemg11b  41902  cdlemg15a  41915  cdlemg15  41916  cdlemg39  41976  trlcone  41988  cdlemg42  41989  tendoconid  42089  tendotr  42090  cdlemk39u  42228  cdlemk19u  42230  tendoex  42235  cdlemm10N  42378  dihord2pre  42485  dihord4  42518  dihord5b  42519  dihglbcpreN  42560  dihmeetlem13N  42579  dih1dimatlem0  42588  mzpcong  44183  jm2.25lem1  44209  jm2.26  44213  idomsubgmo  44398  uhgrimisgrgric  49244  itscnhlinecirc02plem2  50110