Theorem simpr1l 1247

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 782	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 1205	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp2  8141  poxp3  8148  oppccatid  17777  subccatid  17905  setccatid  18143  catccatid  18165  estrccatid  18190  xpccatid  18246  gsmsymgreqlem1  19502  dmdprdsplit  20121  neiptopnei  23260  neitr  23308  neitx  23735  tx1stc  23778  utop3cls  24379  metustsym  24683  ax5seg  29231  clwwlkccat  30284  3pthdlem1  30458  esumpcvgval  34415  esum2d  34430  ifscgr  36471  brofs2  36504  brifs2  36505  btwnconn1lem8  36521  btwnconn1lem12  36525  seglecgr12im  36537  unbdqndv2  37025  lhp2lt  40702  cdlemd1  40899  cdleme3b  40930  cdleme3c  40931  cdleme3e  40933  cdlemf2  41263  cdlemg4c  41313  cdlemn11pre  41911  dihmeetlem12N  42019  stoweidlem60  46703  ssccatid  49772  isthincd2  50137  mndtccatid  50287