Theorem simpr1l 1231

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp2  8168  poxp3  8175  oppccatid  17762  subccatid  17891  setccatid  18129  catccatid  18151  estrccatid  18176  xpccatid  18233  gsmsymgreqlem1  19448  dmdprdsplit  20067  neiptopnei  23140  neitr  23188  neitx  23615  tx1stc  23658  utop3cls  24260  metustsym  24568  ax5seg  28953  clwwlkccat  30009  3pthdlem1  30183  esumpcvgval  34079  esum2d  34094  ifscgr  36045  brofs2  36078  brifs2  36079  btwnconn1lem8  36095  btwnconn1lem12  36099  seglecgr12im  36111  unbdqndv2  36512  lhp2lt  40003  cdlemd1  40200  cdleme3b  40231  cdleme3c  40232  cdleme3e  40234  cdlemf2  40564  cdlemg4c  40614  cdlemn11pre  41212  dihmeetlem12N  41320  stoweidlem60  46075  isthincd2  49086  mndtccatid  49184