Theorem simpll2 1063

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

Assertion

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

Proof of Theorem simpll2

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

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

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 1006

This theorem is referenced by:  fidceq  7056  fidifsnen  7057  en2eqpr  7099  iunfidisj  7145  ctssdc  7312  cauappcvgprlemlol  7867  caucvgprlemlol  7890  caucvgprprlemlol  7918  elfzonelfzo  10475  qbtwnre  10516  nn0ltexp2  10971  hashun  11068  swrdclg  11231  xrmaxltsup  11819  subcn2  11872  prodmodclem2  12139  divalglemex  12484  divalglemeuneg  12485  dvdslegcd  12536  lcmledvds  12643  modprmn0modprm0  12830  qexpz  12926  rnglidlmcl  14496  iscnp4  14944  cnrest2  14962  blssps  15153  blss  15154  bdbl  15229  metcnp3  15237  addcncntoplem  15287  cdivcncfap  15330  lgsfcl2  15737  lgsdir  15766  lgsne0  15769  subupgr  16126  clwwlknonex2  16292