Theorem simpll2 1068

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

Assertion

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

Proof of Theorem simpll2

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

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

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 1011

This theorem is referenced by:  fidceq  7165  fidifsnen  7166  en2eqpr  7208  iunfidisj  7254  fdcf1  7310  ctssdc  7447  cauappcvgprlemlol  8008  caucvgprlemlol  8031  caucvgprprlemlol  8059  elfzonelfzo  10631  qbtwnre  10674  nn0ltexp2  11130  hashun  11228  swrdclg  11405  xrmaxltsup  12007  subcn2  12060  prodmodclem2  12327  divalglemex  12672  divalglemeuneg  12673  dvdslegcd  12724  lcmledvds  12831  modprmn0modprm0  13018  qexpz  13114  rnglidlmcl  14800  iscnp4  15302  cnrest2  15320  blssps  15511  blss  15512  bdbl  15587  metcnp3  15595  addcncntoplem  15645  cdivcncfap  15688  lgsfcl2  16108  lgsdir  16137  lgsne0  16140  subupgr  16497  clwwlknonex2  16663