Theorem simpll2 1068

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

Assertion

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

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1032	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜓)
2	1	adantr 276	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidceq  7171  fidifsnen  7172  en2eqpr  7214  iunfidisj  7260  fdcf1  7316  ctssdc  7453  cauappcvgprlemlol  8014  caucvgprlemlol  8037  caucvgprprlemlol  8065  elfzonelfzo  10650  qbtwnre  10693  nn0ltexp2  11149  hashun  11247  swrdclg  11424  xrmaxltsup  12026  subcn2  12079  prodmodclem2  12346  divalglemex  12691  divalglemeuneg  12692  dvdslegcd  12743  lcmledvds  12850  modprmn0modprm0  13037  qexpz  13133  rnglidlmcl  14819  iscnp4  15321  cnrest2  15339  blssps  15530  blss  15531  bdbl  15606  metcnp3  15614  addcncntoplem  15664  cdivcncfap  15707  lgsfcl2  16137  lgsdir  16166  lgsne0  16169  subupgr  16526  clwwlknonex2  16692