Theorem simpr2l 1232

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr2l	⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr2l

Step	Hyp	Ref	Expression
1		simprl 770	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr2 1189	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  poxp2  8169  ttrcltr  9757  ttrclss  9761  dmttrcl  9762  ttrclselem2  9767  oppccatid  17763  subccatid  17892  setccatid  18130  catccatid  18152  estrccatid  18177  xpccatid  18234  kerf1ghm  19266  gsmsymgreqlem1  19449  nllyidm  23498  noinfbnd1lem5  27773  ax5seg  28954  3pthdlem1  30184  segconeq  36012  ifscgr  36046  brofs2  36079  brifs2  36080  idinside  36086  btwnconn1lem8  36096  btwnconn1lem12  36100  segcon2  36107  segletr  36116  outsidele  36134  unbdqndv2  36513  lplnexllnN  39567  paddasslem9  39831  pmodlem2  39850  lhp2lt  40004  cdlemc3  40196  cdlemc4  40197  cdlemd1  40201  cdleme3b  40232  cdleme3c  40233  cdleme42ke  40488  cdlemg4c  40615  clnbgrgrimlem  47906  isthincd2  49111  mndtccatid  49239