Theorem simpr1l 1249

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

Assertion

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

Proof of Theorem simpr1l

Step	Hyp	Ref	Expression
1		simprl 783	. 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  poxp3  8151  oppccatid  17873  subccatid  18001  setccatid  18239  catccatid  18261  estrccatid  18286  xpccatid  18342  gsmsymgreqlem1  19624  dmdprdsplit  20243  neiptopnei  23430  neitr  23478  neitx  23906  tx1stc  23949  utop3cls  24550  metustsym  24854  ax5seg  29498  clwwlkccat  30563  3pthdlem1  30747  esumpcvgval  34692  esum2d  34707  ifscgr  36779  brofs2  36812  brifs2  36813  btwnconn1lem8  36829  btwnconn1lem12  36833  seglecgr12im  36845  unbdqndv2  37347  lhp2lt  41026  cdlemd1  41223  cdleme3b  41254  cdleme3c  41255  cdleme3e  41257  cdlemf2  41587  cdlemg4c  41637  cdlemn11pre  42235  dihmeetlem12N  42343  stoweidlem60  47014  ssccatid  50124  isthincd2  50489  mndtccatid  50639