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  6939  fidifsnen  6940  en2eqpr  6977  iunfidisj  7021  ctssdc  7188  cauappcvgprlemlol  7733  caucvgprlemlol  7756  caucvgprprlemlol  7784  elfzonelfzo  10325  qbtwnre  10365  nn0ltexp2  10820  hashun  10916  xrmaxltsup  11442  subcn2  11495  prodmodclem2  11761  divalglemex  12106  divalglemeuneg  12107  dvdslegcd  12158  lcmledvds  12265  modprmn0modprm0  12452  qexpz  12548  rnglidlmcl  14114  iscnp4  14562  cnrest2  14580  blssps  14771  blss  14772  bdbl  14847  metcnp3  14855  addcncntoplem  14905  cdivcncfap  14948  lgsfcl2  15355  lgsdir  15384  lgsne0  15387