Theorem simpl2r 1226

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

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  soisores  7207  omopth2  8424  ttrcltr  9483  fin23lem11  10082  xmulasslem3  13029  ssfzo12bi  13491  ntrivcvgmul  15623  pockthg  16616  gsumsgrpccat  18487  efgred  19363  lspfixed  20399  decpmatmullem  21929  decpmatmul  21930  unconn  22589  llyrest  22645  basqtop  22871  tmdgsum  23255  tsmsxp  23315  ucncn  23446  mulcxp  25849  cxple2  25861  ax5seglem1  27305  ax5seglem2  27306  axpasch  27318  axcontlem4  27344  1pthon2v  28526  cvmlift2lem10  33283  br4  33734  nogt01o  33908  noetalem1  33953  cofcut1  34099  cgrcomim  34300  btwnintr  34330  btwnouttr2  34333  btwndiff  34338  btwnconn1lem14  34411  btwnconn3  34414  segcon2  34416  brsegle  34419  brsegle2  34420  segleantisym  34426  outsideofeu  34442  eqlkr  37120  eqlkr2  37121  lkrlsp  37123  atbtwn  37467  3dimlem3OLDN  37483  3dim3  37490  3atlem7  37510  4atlem0a  37614  4atlem3a  37618  4atlem11  37630  lneq2at  37799  lnatexN  37800  paddasslem6  37846  llnexchb2  37890  lhpexle2lem  38030  lhpexle3  38033  lhp2at0nle  38056  lhpat3  38067  trlnid  38200  ltrneq3  38229  cdleme17b  38308  cdleme27cl  38387  cdlemefrs29bpre0  38417  cdlemefrs29clN  38420  cdlemefrs32fva  38421  cdlemefs32sn1aw  38435  cdleme32le  38468  ltrniotavalbN  38605  cdlemg6  38644  cdlemg7N  38647  cdlemg11b  38663  cdlemg15a  38676  cdlemg15  38677  cdlemg39  38737  trlcone  38749  cdlemg42  38750  tendoconid  38850  tendotr  38851  cdlemk39u  38989  cdlemk19u  38991  tendoex  38996  cdlemm10N  39139  dihord2pre  39246  dihord4  39279  dihord5b  39280  dihglbcpreN  39321  dihmeetlem13N  39340  dih1dimatlem0  39349  mzpcong  40801  jm2.25lem1  40827  jm2.26  40831  idomsubgmo  41030  itscnhlinecirc02plem2  46140