Theorem simpr2l 1229

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

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

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 1086

This theorem is referenced by:  oppccatid  16981  subccatid  17108  setccatid  17336  catccatid  17354  estrccatid  17374  xpccatid  17430  gsmsymgreqlem1  18550  kerf1ghm  19491  nllyidm  22094  ax5seg  26732  3pthdlem1  27949  segconeq  33584  ifscgr  33618  brofs2  33651  brifs2  33652  idinside  33658  btwnconn1lem8  33668  btwnconn1lem12  33672  segcon2  33679  segletr  33688  outsidele  33706  unbdqndv2  33963  lplnexllnN  36860  paddasslem9  37124  pmodlem2  37143  lhp2lt  37297  cdlemc3  37489  cdlemc4  37490  cdlemd1  37494  cdleme3b  37525  cdleme3c  37526  cdleme42ke  37781  cdlemg4c  37908