Theorem simpr2l 1249

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  poxp2  8127  ttrcltr  9673  ttrclss  9677  dmttrcl  9678  ttrclselem2  9683  oppccatid  17765  subccatid  17893  setccatid  18131  catccatid  18153  estrccatid  18178  xpccatid  18234  kerf1ghm  19308  gsmsymgreqlem1  19491  nllyidm  23607  noinfbnd1lem5  27849  ax5seg  29197  3pthdlem1  30424  segconeq  36373  ifscgr  36407  brofs2  36440  brifs2  36441  idinside  36447  btwnconn1lem8  36457  btwnconn1lem12  36461  segcon2  36468  segletr  36477  outsidele  36495  unbdqndv2  36962  lplnexllnN  40200  paddasslem9  40464  pmodlem2  40483  lhp2lt  40637  cdlemc3  40829  cdlemc4  40830  cdlemd1  40834  cdleme3b  40865  cdleme3c  40866  cdleme42ke  41121  cdlemg4c  41248  clnbgrgrimlem  48553  ssccatid  49701  isthincd2  50066  mndtccatid  50216