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  10476  qbtwnre  10517  nn0ltexp2  10972  hashun  11069  swrdclg  11232  xrmaxltsup  11820  subcn2  11873  prodmodclem2  12140  divalglemex  12485  divalglemeuneg  12486  dvdslegcd  12537  lcmledvds  12644  modprmn0modprm0  12831  qexpz  12927  rnglidlmcl  14497  iscnp4  14945  cnrest2  14963  blssps  15154  blss  15155  bdbl  15230  metcnp3  15238  addcncntoplem  15288  cdivcncfap  15331  lgsfcl2  15738  lgsdir  15767  lgsne0  15770  subupgr  16127  clwwlknonex2  16293