Theorem simpll2 1061

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

Assertion

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

Proof of Theorem simpll2

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

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

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 1004

This theorem is referenced by:  fidceq  7051  fidifsnen  7052  en2eqpr  7094  iunfidisj  7139  ctssdc  7306  cauappcvgprlemlol  7860  caucvgprlemlol  7883  caucvgprprlemlol  7911  elfzonelfzo  10468  qbtwnre  10509  nn0ltexp2  10964  hashun  11061  swrdclg  11224  xrmaxltsup  11812  subcn2  11865  prodmodclem2  12131  divalglemex  12476  divalglemeuneg  12477  dvdslegcd  12528  lcmledvds  12635  modprmn0modprm0  12822  qexpz  12918  rnglidlmcl  14487  iscnp4  14935  cnrest2  14953  blssps  15144  blss  15145  bdbl  15220  metcnp3  15228  addcncntoplem  15278  cdivcncfap  15321  lgsfcl2  15728  lgsdir  15757  lgsne0  15760  clwwlknonex2  16248