Theorem simpll2 1064

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

Assertion

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

Proof of Theorem simpll2

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  fidceq  7137  fidifsnen  7138  en2eqpr  7180  iunfidisj  7226  ctssdc  7417  cauappcvgprlemlol  7978  caucvgprlemlol  8001  caucvgprprlemlol  8029  elfzonelfzo  10600  qbtwnre  10643  nn0ltexp2  11099  hashun  11197  swrdclg  11370  xrmaxltsup  11971  subcn2  12024  prodmodclem2  12291  divalglemex  12636  divalglemeuneg  12637  dvdslegcd  12688  lcmledvds  12795  modprmn0modprm0  12982  qexpz  13078  rnglidlmcl  14757  iscnp4  15212  cnrest2  15230  blssps  15421  blss  15422  bdbl  15497  metcnp3  15505  addcncntoplem  15555  cdivcncfap  15598  lgsfcl2  16008  lgsdir  16037  lgsne0  16040  subupgr  16397  clwwlknonex2  16563