Theorem simpr1l 1226

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  oppccatid  16991  subccatid  17118  setccatid  17346  catccatid  17364  estrccatid  17384  xpccatid  17440  gsmsymgreqlem1  18560  dmdprdsplit  19171  neiptopnei  21742  neitr  21790  neitx  22217  tx1stc  22260  utop3cls  22862  metustsym  23167  ax5seg  26726  clwwlkccat  27770  3pthdlem1  27945  esumpcvgval  31339  esum2d  31354  ifscgr  33507  brofs2  33540  brifs2  33541  btwnconn1lem8  33557  btwnconn1lem12  33561  seglecgr12im  33573  unbdqndv2  33852  lhp2lt  37139  cdlemd1  37336  cdleme3b  37367  cdleme3c  37368  cdleme3e  37370  cdlemf2  37700  cdlemg4c  37750  cdlemn11pre  38348  dihmeetlem12N  38456  stoweidlem60  42352