Theorem simpr1l 1229

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 768	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 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 206  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8132  poxp3  8139  oppccatid  17670  subccatid  17801  setccatid  18039  catccatid  18061  estrccatid  18088  xpccatid  18145  gsmsymgreqlem1  19340  dmdprdsplit  19959  neiptopnei  22857  neitr  22905  neitx  23332  tx1stc  23375  utop3cls  23977  metustsym  24285  ax5seg  28464  clwwlkccat  29511  3pthdlem1  29685  esumpcvgval  33375  esum2d  33390  ifscgr  35321  brofs2  35354  brifs2  35355  btwnconn1lem8  35371  btwnconn1lem12  35375  seglecgr12im  35387  unbdqndv2  35691  lhp2lt  39176  cdlemd1  39373  cdleme3b  39404  cdleme3c  39405  cdleme3e  39407  cdlemf2  39737  cdlemg4c  39787  cdlemn11pre  40385  dihmeetlem12N  40493  stoweidlem60  45075  isthincd2  47746  mndtccatid  47801