Theorem simpr1r 1250

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr1r	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜓)

Proof of Theorem simpr1r

Step	Hyp	Ref	Expression
1		simprr 785	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜓)
2	1	3ad2antr1 1207	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:  poxp2  8144  oppccatid  17873  subccatid  18001  setccatid  18239  catccatid  18261  estrccatid  18286  xpccatid  18342  gsmsymgreqlem1  19624  dmdprdsplit  20243  neitr  23478  neitx  23906  tx1stc  23949  utop3cls  24550  metustsym  24854  clwwlkccat  30563  3pthdlem1  30747  archiabllem1  33736  esumpcvgval  34692  esum2d  34707  ifscgr  36779  btwnconn1lem8  36829  btwnconn1lem11  36832  btwnconn1lem12  36833  segletr  36849  broutsideof3  36861  unbdqndv2  37347  lhp2lt  41026  cdlemf2  41587  cdlemn11pre  42235  stoweidlem60  47014  ssccatid  50124  isthincd2  50489  mndtccatid  50639