Theorem simpr2l 1251

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 783	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr2 1208	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8144  ttrcltr  9701  ttrclss  9705  dmttrcl  9706  ttrclselem2  9711  oppccatid  17873  subccatid  18001  setccatid  18239  catccatid  18261  estrccatid  18286  xpccatid  18342  kerf1ghm  19441  gsmsymgreqlem1  19624  nllyidm  23788  noinfbnd1lem5  28066  ax5seg  29498  3pthdlem1  30747  segconeq  36745  ifscgr  36779  brofs2  36812  brifs2  36813  idinside  36819  btwnconn1lem8  36829  btwnconn1lem12  36833  segcon2  36840  segletr  36849  outsidele  36867  unbdqndv2  37347  lplnexllnN  40589  paddasslem9  40853  pmodlem2  40872  lhp2lt  41026  cdlemc3  41218  cdlemc4  41219  cdlemd1  41223  cdleme3b  41254  cdleme3c  41255  cdleme42ke  41510  cdlemg4c  41637  clnbgrgrimlem  48975  ssccatid  50124  isthincd2  50489  mndtccatid  50639