Theorem simpr1l 1232

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 1190	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  8086  poxp3  8093  oppccatid  17676  subccatid  17804  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  gsmsymgreqlem1  19396  dmdprdsplit  20015  neiptopnei  23107  neitr  23155  neitx  23582  tx1stc  23625  utop3cls  24226  metustsym  24530  ax5seg  29021  clwwlkccat  30075  3pthdlem1  30249  esumpcvgval  34238  esum2d  34253  ifscgr  36242  brofs2  36275  brifs2  36276  btwnconn1lem8  36292  btwnconn1lem12  36296  seglecgr12im  36308  unbdqndv2  36787  lhp2lt  40461  cdlemd1  40658  cdleme3b  40689  cdleme3c  40690  cdleme3e  40692  cdlemf2  41022  cdlemg4c  41072  cdlemn11pre  41670  dihmeetlem12N  41778  stoweidlem60  46506  ssccatid  49559  isthincd2  49924  mndtccatid  50074