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  7327  omopth2  8576  ttrcltr  9701  fin23lem11  10376  xmulasslem3  13397  ssfzo12bi  13876  ntrivcvgmul  16051  pockthg  17064  gsumsgrpccat  19016  efgred  19942  lspfixed  21386  decpmatmullem  23069  decpmatmul  23070  unconn  23727  llyrest  23784  basqtop  24010  tmdgsum  24394  tsmsxp  24454  ucncn  24583  mulcxp  26995  cxple2  27007  nogt01o  28035  noetalem1  28080  cofcut1  28288  bdayfinbndlem1  28835  ax5seglem1  29488  ax5seglem2  29489  axpasch  29501  axcontlem4  29527  1pthon2v  30736  mhmimasplusg  33580  cvmlift2lem10  36046  br4  36492  cgrcomim  36724  btwnintr  36754  btwnouttr2  36757  btwndiff  36762  btwnconn1lem14  36835  btwnconn3  36838  segcon2  36840  brsegle  36843  brsegle2  36844  segleantisym  36850  outsideofeu  36866  eqlkr  40124  eqlkr2  40125  lkrlsp  40127  atbtwn  40471  3dimlem3OLDN  40487  3dim3  40494  3atlem7  40514  4atlem0a  40618  4atlem3a  40622  4atlem11  40634  lneq2at  40803  lnatexN  40804  paddasslem6  40850  llnexchb2  40894  lhpexle2lem  41034  lhpexle3  41037  lhp2at0nle  41060  lhpat3  41071  trlnid  41204  ltrneq3  41233  cdleme17b  41312  cdleme27cl  41391  cdlemefrs29bpre0  41421  cdlemefrs29clN  41424  cdlemefrs32fva  41425  cdlemefs32sn1aw  41439  cdleme32le  41472  ltrniotavalbN  41609  cdlemg6  41648  cdlemg7N  41651  cdlemg11b  41667  cdlemg15a  41680  cdlemg15  41681  cdlemg39  41741  trlcone  41753  cdlemg42  41754  tendoconid  41854  tendotr  41855  cdlemk39u  41993  cdlemk19u  41995  tendoex  42000  cdlemm10N  42143  dihord2pre  42250  dihord4  42283  dihord5b  42284  dihglbcpreN  42325  dihmeetlem13N  42344  dih1dimatlem0  42353  mzpcong  43932  jm2.25lem1  43958  jm2.26  43962  idomsubgmo  44153  uhgrimisgrgric  48973  itscnhlinecirc02plem2  49839