Theorem simpr2l 1113

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

Assertion

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

Proof of Theorem simpr2l

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  oppccatid  16202  subccatid  16329  setccatid  16557  catccatid  16575  estrccatid  16595  xpccatid  16651  gsmsymgreqlem1  17673  kerf1hrm  18566  nllyidm  21102  ax5seg  25618  segconeq  31287  ifscgr  31321  brofs2  31354  brifs2  31355  idinside  31361  btwnconn1lem8  31371  btwnconn1lem12  31375  segcon2  31382  segletr  31391  outsidele  31409  unbdqndv2  31672  lplnexllnN  33868  paddasslem9  34132  pmodlem2  34151  lhp2lt  34305  cdlemc3  34498  cdlemc4  34499  cdlemd1  34503  cdleme3b  34534  cdleme3c  34535  cdleme42ke  34791  cdlemg4c  34918  3pthdlem1  41331