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  8086  ttrcltr  9628  ttrclss  9632  dmttrcl  9633  ttrclselem2  9638  oppccatid  17676  subccatid  17804  setccatid  18042  catccatid  18064  estrccatid  18089  xpccatid  18145  kerf1ghm  19213  gsmsymgreqlem1  19396  nllyidm  23464  noinfbnd1lem5  27705  ax5seg  29021  3pthdlem1  30249  segconeq  36208  ifscgr  36242  brofs2  36275  brifs2  36276  idinside  36282  btwnconn1lem8  36292  btwnconn1lem12  36296  segcon2  36303  segletr  36312  outsidele  36330  unbdqndv2  36787  lplnexllnN  40024  paddasslem9  40288  pmodlem2  40307  lhp2lt  40461  cdlemc3  40653  cdlemc4  40654  cdlemd1  40658  cdleme3b  40689  cdleme3c  40690  cdleme42ke  40945  cdlemg4c  41072  clnbgrgrimlem  48421  ssccatid  49559  isthincd2  49924  mndtccatid  50074