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  7061  fidifsnen  7062  en2eqpr  7104  iunfidisj  7150  ctssdc  7317  cauappcvgprlemlol  7872  caucvgprlemlol  7895  caucvgprprlemlol  7923  elfzonelfzo  10481  qbtwnre  10522  nn0ltexp2  10977  hashun  11074  swrdclg  11240  xrmaxltsup  11841  subcn2  11894  prodmodclem2  12161  divalglemex  12506  divalglemeuneg  12507  dvdslegcd  12558  lcmledvds  12665  modprmn0modprm0  12852  qexpz  12948  rnglidlmcl  14518  iscnp4  14971  cnrest2  14989  blssps  15180  blss  15181  bdbl  15256  metcnp3  15264  addcncntoplem  15314  cdivcncfap  15357  lgsfcl2  15764  lgsdir  15793  lgsne0  15796  subupgr  16153  clwwlknonex2  16319