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  7044  fidifsnen  7045  en2eqpr  7085  iunfidisj  7129  ctssdc  7296  cauappcvgprlemlol  7850  caucvgprlemlol  7873  caucvgprprlemlol  7901  elfzonelfzo  10453  qbtwnre  10493  nn0ltexp2  10948  hashun  11044  swrdclg  11203  xrmaxltsup  11790  subcn2  11843  prodmodclem2  12109  divalglemex  12454  divalglemeuneg  12455  dvdslegcd  12506  lcmledvds  12613  modprmn0modprm0  12800  qexpz  12896  rnglidlmcl  14465  iscnp4  14913  cnrest2  14931  blssps  15122  blss  15123  bdbl  15198  metcnp3  15206  addcncntoplem  15256  cdivcncfap  15299  lgsfcl2  15706  lgsdir  15735  lgsne0  15738