Theorem simpl2r 1234

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

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

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 1094

This theorem is referenced by:  soisores  7278  omopth2  8516  ttrcltr  9635  fin23lem11  10237  xmulasslem3  13236  ssfzo12bi  13714  ntrivcvgmul  15865  pockthg  16875  gsumsgrpccat  18806  efgred  19721  lspfixed  21128  decpmatmullem  22761  decpmatmul  22762  unconn  23419  llyrest  23475  basqtop  23701  tmdgsum  24085  tsmsxp  24145  ucncn  24274  mulcxp  26674  cxple2  26686  nogt01o  27685  noetalem1  27730  cofcut1  27937  bdayfinbndlem1  28484  ax5seglem1  29022  ax5seglem2  29023  axpasch  29035  axcontlem4  29061  1pthon2v  30248  mhmimasplusg  33124  cvmlift2lem10  35547  br4  35993  cgrcomim  36224  btwnintr  36254  btwnouttr2  36257  btwndiff  36262  btwnconn1lem14  36335  btwnconn3  36338  segcon2  36340  brsegle  36343  brsegle2  36344  segleantisym  36350  outsideofeu  36366  eqlkr  39598  eqlkr2  39599  lkrlsp  39601  atbtwn  39945  3dimlem3OLDN  39961  3dim3  39968  3atlem7  39988  4atlem0a  40092  4atlem3a  40096  4atlem11  40108  lneq2at  40277  lnatexN  40278  paddasslem6  40324  llnexchb2  40368  lhpexle2lem  40508  lhpexle3  40511  lhp2at0nle  40534  lhpat3  40545  trlnid  40678  ltrneq3  40707  cdleme17b  40786  cdleme27cl  40865  cdlemefrs29bpre0  40895  cdlemefrs29clN  40898  cdlemefrs32fva  40899  cdlemefs32sn1aw  40913  cdleme32le  40946  ltrniotavalbN  41083  cdlemg6  41122  cdlemg7N  41125  cdlemg11b  41141  cdlemg15a  41154  cdlemg15  41155  cdlemg39  41215  trlcone  41227  cdlemg42  41228  tendoconid  41328  tendotr  41329  cdlemk39u  41467  cdlemk19u  41469  tendoex  41474  cdlemm10N  41617  dihord2pre  41724  dihord4  41757  dihord5b  41758  dihglbcpreN  41799  dihmeetlem13N  41818  dih1dimatlem0  41827  mzpcong  43424  jm2.25lem1  43450  jm2.26  43454  idomsubgmo  43645  uhgrimisgrgric  48429  itscnhlinecirc02plem2  49281