Theorem simpr2l 1234

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 1191	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp2  8095  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  ttrclselem2  9647  oppccatid  17654  subccatid  17782  setccatid  18020  catccatid  18042  estrccatid  18067  xpccatid  18123  kerf1ghm  19188  gsmsymgreqlem1  19371  nllyidm  23445  noinfbnd1lem5  27707  ax5seg  29023  3pthdlem1  30251  segconeq  36223  ifscgr  36257  brofs2  36290  brifs2  36291  idinside  36297  btwnconn1lem8  36307  btwnconn1lem12  36311  segcon2  36318  segletr  36327  outsidele  36345  unbdqndv2  36730  lplnexllnN  39934  paddasslem9  40198  pmodlem2  40217  lhp2lt  40371  cdlemc3  40563  cdlemc4  40564  cdlemd1  40568  cdleme3b  40599  cdleme3c  40600  cdleme42ke  40855  cdlemg4c  40982  clnbgrgrimlem  48287  ssccatid  49425  isthincd2  49790  mndtccatid  49940