Theorem simpl2r 1228

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  soisores  7261  omopth2  8499  ttrcltr  9606  fin23lem11  10205  xmulasslem3  13182  ssfzo12bi  13658  ntrivcvgmul  15806  pockthg  16815  gsumsgrpccat  18745  efgred  19658  lspfixed  21063  decpmatmullem  22684  decpmatmul  22685  unconn  23342  llyrest  23398  basqtop  23624  tmdgsum  24008  tsmsxp  24068  ucncn  24197  mulcxp  26619  cxple2  26631  nogt01o  27633  noetalem1  27678  cofcut1  27862  ax5seglem1  28904  ax5seglem2  28905  axpasch  28917  axcontlem4  28943  1pthon2v  30128  mhmimasplusg  33014  cvmlift2lem10  35344  br4  35790  cgrcomim  36022  btwnintr  36052  btwnouttr2  36055  btwndiff  36060  btwnconn1lem14  36133  btwnconn3  36136  segcon2  36138  brsegle  36141  brsegle2  36142  segleantisym  36148  outsideofeu  36164  eqlkr  39137  eqlkr2  39138  lkrlsp  39140  atbtwn  39484  3dimlem3OLDN  39500  3dim3  39507  3atlem7  39527  4atlem0a  39631  4atlem3a  39635  4atlem11  39647  lneq2at  39816  lnatexN  39817  paddasslem6  39863  llnexchb2  39907  lhpexle2lem  40047  lhpexle3  40050  lhp2at0nle  40073  lhpat3  40084  trlnid  40217  ltrneq3  40246  cdleme17b  40325  cdleme27cl  40404  cdlemefrs29bpre0  40434  cdlemefrs29clN  40437  cdlemefrs32fva  40438  cdlemefs32sn1aw  40452  cdleme32le  40485  ltrniotavalbN  40622  cdlemg6  40661  cdlemg7N  40664  cdlemg11b  40680  cdlemg15a  40693  cdlemg15  40694  cdlemg39  40754  trlcone  40766  cdlemg42  40767  tendoconid  40867  tendotr  40868  cdlemk39u  41006  cdlemk19u  41008  tendoex  41013  cdlemm10N  41156  dihord2pre  41263  dihord4  41296  dihord5b  41297  dihglbcpreN  41338  dihmeetlem13N  41357  dih1dimatlem0  41366  mzpcong  43004  jm2.25lem1  43030  jm2.26  43034  idomsubgmo  43225  uhgrimisgrgric  47961  itscnhlinecirc02plem2  48814