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  8073  ttrcltr  9606  ttrclss  9610  dmttrcl  9611  ttrclselem2  9616  oppccatid  17622  subccatid  17750  setccatid  17988  catccatid  18010  estrccatid  18035  xpccatid  18091  kerf1ghm  19157  gsmsymgreqlem1  19340  nllyidm  23402  noinfbnd1lem5  27664  ax5seg  28914  3pthdlem1  30139  segconeq  36043  ifscgr  36077  brofs2  36110  brifs2  36111  idinside  36117  btwnconn1lem8  36127  btwnconn1lem12  36131  segcon2  36138  segletr  36147  outsidele  36165  unbdqndv2  36544  lplnexllnN  39602  paddasslem9  39866  pmodlem2  39885  lhp2lt  40039  cdlemc3  40231  cdlemc4  40232  cdlemd1  40236  cdleme3b  40267  cdleme3c  40268  cdleme42ke  40523  cdlemg4c  40650  clnbgrgrimlem  47963  ssccatid  49103  isthincd2  49468  mndtccatid  49618