Theorem simpr2l 1233

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 1190	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  8079  ttrcltr  9613  ttrclss  9617  dmttrcl  9618  ttrclselem2  9623  oppccatid  17627  subccatid  17755  setccatid  17993  catccatid  18015  estrccatid  18040  xpccatid  18096  kerf1ghm  19161  gsmsymgreqlem1  19344  nllyidm  23405  noinfbnd1lem5  27667  ax5seg  28918  3pthdlem1  30146  segconeq  36075  ifscgr  36109  brofs2  36142  brifs2  36143  idinside  36149  btwnconn1lem8  36159  btwnconn1lem12  36163  segcon2  36170  segletr  36179  outsidele  36197  unbdqndv2  36576  lplnexllnN  39683  paddasslem9  39947  pmodlem2  39966  lhp2lt  40120  cdlemc3  40312  cdlemc4  40313  cdlemd1  40317  cdleme3b  40348  cdleme3c  40349  cdleme42ke  40604  cdlemg4c  40731  clnbgrgrimlem  48057  ssccatid  49197  isthincd2  49562  mndtccatid  49712