Theorem simpr2l 1266

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  oppccatid  16764  subccatid  16891  setccatid  17119  catccatid  17137  estrccatid  17157  xpccatid  17214  gsmsymgreqlem1  18233  kerf1ghm  19134  kerf1hrmOLD  19135  nllyidm  21701  ax5seg  26287  3pthdlem1  27581  segconeq  32720  ifscgr  32754  brofs2  32787  brifs2  32788  idinside  32794  btwnconn1lem8  32804  btwnconn1lem12  32808  segcon2  32815  segletr  32824  outsidele  32842  unbdqndv2  33098  lplnexllnN  35712  paddasslem9  35976  pmodlem2  35995  lhp2lt  36149  cdlemc3  36341  cdlemc4  36342  cdlemd1  36346  cdleme3b  36377  cdleme3c  36378  cdleme42ke  36633  cdlemg4c  36760