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  8141  ttrcltr  9687  ttrclss  9691  dmttrcl  9692  ttrclselem2  9697  oppccatid  17777  subccatid  17905  setccatid  18143  catccatid  18165  estrccatid  18190  xpccatid  18246  kerf1ghm  19319  gsmsymgreqlem1  19502  nllyidm  23617  noinfbnd1lem5  27859  ax5seg  29231  3pthdlem1  30458  segconeq  36437  ifscgr  36471  brofs2  36504  brifs2  36505  idinside  36511  btwnconn1lem8  36521  btwnconn1lem12  36525  segcon2  36532  segletr  36541  outsidele  36559  unbdqndv2  37025  lplnexllnN  40265  paddasslem9  40529  pmodlem2  40548  lhp2lt  40702  cdlemc3  40894  cdlemc4  40895  cdlemd1  40899  cdleme3b  40930  cdleme3c  40931  cdleme42ke  41186  cdlemg4c  41313  clnbgrgrimlem  48624  ssccatid  49772  isthincd2  50137  mndtccatid  50287