Theorem simpl2r 1220

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  soisores  6948  omopth2  8065  fin23lem11  9590  xmulasslem3  12534  ssfzo12bi  12987  ntrivcvgmul  15096  pockthg  16076  gsmsymgreqlem2  18295  efgred  18606  lspfixed  19595  decpmatmullem  21068  decpmatmul  21069  unconn  21726  llyrest  21782  basqtop  22008  tmdgsum  22392  tsmsxp  22451  ucncn  22582  mulcxp  24954  cxple2  24966  ax5seglem1  26402  ax5seglem2  26403  axpasch  26415  axcontlem4  26441  1pthon2v  27624  cvmlift2lem10  32173  br4  32608  cgrcomim  33065  btwnintr  33095  btwnouttr2  33098  btwndiff  33103  btwnconn1lem14  33176  btwnconn3  33179  segcon2  33181  brsegle  33184  brsegle2  33185  segleantisym  33191  outsideofeu  33207  eqlkr  35791  eqlkr2  35792  lkrlsp  35794  atbtwn  36138  3dimlem3OLDN  36154  3dim3  36161  3atlem7  36181  4atlem0a  36285  4atlem3a  36289  4atlem11  36301  lneq2at  36470  lnatexN  36471  paddasslem6  36517  llnexchb2  36561  lhpexle2lem  36701  lhpexle3  36704  lhp2at0nle  36727  lhpat3  36738  trlnid  36871  ltrneq3  36900  cdleme17b  36979  cdleme27cl  37058  cdlemefrs29bpre0  37088  cdlemefrs29clN  37091  cdlemefrs32fva  37092  cdlemefs32sn1aw  37106  cdleme32le  37139  ltrniotavalbN  37276  cdlemg6  37315  cdlemg7N  37318  cdlemg11b  37334  cdlemg15a  37347  cdlemg15  37348  cdlemg39  37408  trlcone  37420  cdlemg42  37421  tendoconid  37521  tendotr  37522  cdlemk39u  37660  cdlemk19u  37662  tendoex  37667  cdlemm10N  37810  dihord2pre  37917  dihord4  37950  dihord5b  37951  dihglbcpreN  37992  dihmeetlem13N  38011  dih1dimatlem0  38020  mzpcong  39079  jm2.25lem1  39105  jm2.26  39109  idomsubgmo  39308  itscnhlinecirc02plem2  44277