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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  oppccatid  17096  subccatid  17224  setccatid  17459  catccatid  17481  estrccatid  17501  xpccatid  17557  gsmsymgreqlem1  18679  kerf1ghm  19620  nllyidm  22243  ax5seg  26887  3pthdlem1  28104  poxp2  33406  noinfbnd1lem5  33576  segconeq  33958  ifscgr  33992  brofs2  34025  brifs2  34026  idinside  34032  btwnconn1lem8  34042  btwnconn1lem12  34046  segcon2  34053  segletr  34062  outsidele  34080  unbdqndv2  34337  lplnexllnN  37224  paddasslem9  37488  pmodlem2  37507  lhp2lt  37661  cdlemc3  37853  cdlemc4  37854  cdlemd1  37858  cdleme3b  37889  cdleme3c  37890  cdleme42ke  38145  cdlemg4c  38272  isthincd2  45822  mndtccatid  45857