Theorem simpll2 1039

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

Assertion

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

Proof of Theorem simpll2

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

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

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 982

This theorem is referenced by:  fidceq  6930  fidifsnen  6931  en2eqpr  6968  iunfidisj  7012  ctssdc  7179  cauappcvgprlemlol  7714  caucvgprlemlol  7737  caucvgprprlemlol  7765  elfzonelfzo  10306  qbtwnre  10346  nn0ltexp2  10801  hashun  10897  xrmaxltsup  11423  subcn2  11476  prodmodclem2  11742  divalglemex  12087  divalglemeuneg  12088  dvdslegcd  12131  lcmledvds  12238  modprmn0modprm0  12425  qexpz  12521  rnglidlmcl  14036  iscnp4  14454  cnrest2  14472  blssps  14663  blss  14664  bdbl  14739  metcnp3  14747  addcncntoplem  14797  cdivcncfap  14840  lgsfcl2  15247  lgsdir  15276  lgsne0  15279