Theorem simpr2r 1114

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

Assertion

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

Proof of Theorem simpr2r

Step	Hyp	Ref	Expression
1		simp2r 1081	. 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  ax5seg  25618  segconeq  31287  ifscgr  31321  brofs2  31354  brifs2  31355  idinside  31361  btwnconn1lem8  31371  btwnconn1lem11  31374  btwnconn1lem12  31375  segcon2  31382  seglecgr12im  31387  unbdqndv2  31672  lplnexllnN  33868  paddasslem9  34132  paddasslem15  34138  pmodlem2  34151  lhp2lt  34305  3pthdlem1  41331