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  8093  ttrcltr  9637  ttrclss  9641  dmttrcl  9642  ttrclselem2  9647  oppccatid  17685  subccatid  17813  setccatid  18051  catccatid  18073  estrccatid  18098  xpccatid  18154  kerf1ghm  19222  gsmsymgreqlem1  19405  nllyidm  23454  noinfbnd1lem5  27691  ax5seg  29007  3pthdlem1  30234  segconeq  36192  ifscgr  36226  brofs2  36259  brifs2  36260  idinside  36266  btwnconn1lem8  36276  btwnconn1lem12  36280  segcon2  36287  segletr  36296  outsidele  36314  unbdqndv2  36771  lplnexllnN  40010  paddasslem9  40274  pmodlem2  40293  lhp2lt  40447  cdlemc3  40639  cdlemc4  40640  cdlemd1  40644  cdleme3b  40675  cdleme3c  40676  cdleme42ke  40931  cdlemg4c  41058  clnbgrgrimlem  48409  ssccatid  49547  isthincd2  49912  mndtccatid  50062