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  7176  fidifsnen  7177  en2eqpr  7219  iunfidisj  7265  fdcf1  7322  ctssdc  7460  cauappcvgprlemlol  8021  caucvgprlemlol  8044  caucvgprprlemlol  8072  elfzonelfzo  10666  qbtwnre  10709  nn0ltexp2  11170  hashun  11268  swrdclg  11445  xrmaxltsup  12050  subcn2  12103  prodmodclem2  12370  divalglemex  12715  divalglemeuneg  12716  dvdslegcd  12767  lcmledvds  12874  modprmn0modprm0  13065  qexpz  13161  rnglidlmcl  14927  iscnp4  15456  cnrest2  15474  blssps  15665  blss  15666  bdbl  15741  metcnp3  15749  addcncntoplem  15799  cdivcncfap  15842  lgsfcl2  16342  lgsdir  16371  lgsne0  16374  subupgr  16731  clwwlknonex2  16897