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  8147  ttrcltr  9735  ttrclss  9739  dmttrcl  9740  ttrclselem2  9745  oppccatid  17736  subccatid  17864  setccatid  18102  catccatid  18124  estrccatid  18149  xpccatid  18205  kerf1ghm  19235  gsmsymgreqlem1  19416  nllyidm  23432  noinfbnd1lem5  27696  ax5seg  28922  3pthdlem1  30150  segconeq  36033  ifscgr  36067  brofs2  36100  brifs2  36101  idinside  36107  btwnconn1lem8  36117  btwnconn1lem12  36121  segcon2  36128  segletr  36137  outsidele  36155  unbdqndv2  36534  lplnexllnN  39588  paddasslem9  39852  pmodlem2  39871  lhp2lt  40025  cdlemc3  40217  cdlemc4  40218  cdlemd1  40222  cdleme3b  40253  cdleme3c  40254  cdleme42ke  40509  cdlemg4c  40636  clnbgrgrimlem  47913  ssccatid  49006  isthincd2  49290  mndtccatid  49431