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  8187  ttrcltr  9744  ttrclss  9748  dmttrcl  9749  ttrclselem2  9754  oppccatid  17922  subccatid  18050  setccatid  18288  catccatid  18310  estrccatid  18335  xpccatid  18391  kerf1ghm  19490  gsmsymgreqlem1  19674  nllyidm  23838  noinfbnd1lem5  28114  ax5seg  29546  3pthdlem1  30795  segconeq  36953  ifscgr  36987  brofs2  37020  brifs2  37021  idinside  37027  btwnconn1lem8  37037  btwnconn1lem12  37041  segcon2  37048  segletr  37057  outsidele  37075  unbdqndv2  37555  lplnexllnN  40813  paddasslem9  41077  pmodlem2  41096  lhp2lt  41250  cdlemc3  41442  cdlemc4  41443  cdlemd1  41447  cdleme3b  41478  cdleme3c  41479  cdleme42ke  41734  cdlemg4c  41861  clnbgrgrimlem  49236  ssccatid  50391  isthincd2  50777  mndtccatid  50930