Theorem simpr2l 1120

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpr2l	⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr2l

Step	Hyp	Ref	Expression
1		simp2l 1087	. 2 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜑)
2	1	adantl 482	1 ⊢ ((𝜏 ∧ (𝜒 ∧ (𝜑 ∧ 𝜓) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  oppccatid  16379  subccatid  16506  setccatid  16734  catccatid  16752  estrccatid  16772  xpccatid  16828  gsmsymgreqlem1  17850  kerf1hrm  18743  nllyidm  21292  ax5seg  25818  3pthdlem1  27024  segconeq  32117  ifscgr  32151  brofs2  32184  brifs2  32185  idinside  32191  btwnconn1lem8  32201  btwnconn1lem12  32205  segcon2  32212  segletr  32221  outsidele  32239  unbdqndv2  32502  lplnexllnN  34850  paddasslem9  35114  pmodlem2  35133  lhp2lt  35287  cdlemc3  35480  cdlemc4  35481  cdlemd1  35485  cdleme3b  35516  cdleme3c  35517  cdleme42ke  35773  cdlemg4c  35900