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  7123  fidifsnen  7124  en2eqpr  7166  iunfidisj  7212  ctssdc  7403  cauappcvgprlemlol  7958  caucvgprlemlol  7981  caucvgprprlemlol  8009  elfzonelfzo  10571  qbtwnre  10612  nn0ltexp2  11067  hashun  11164  swrdclg  11335  xrmaxltsup  11936  subcn2  11989  prodmodclem2  12256  divalglemex  12601  divalglemeuneg  12602  dvdslegcd  12653  lcmledvds  12760  modprmn0modprm0  12947  qexpz  13043  rnglidlmcl  14615  iscnp4  15070  cnrest2  15088  blssps  15279  blss  15280  bdbl  15355  metcnp3  15363  addcncntoplem  15413  cdivcncfap  15456  lgsfcl2  15866  lgsdir  15895  lgsne0  15898  subupgr  16255  clwwlknonex2  16421