Theorem simpll2 1022

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

Assertion

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

Proof of Theorem simpll2

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  fidceq  6816  fidifsnen  6817  en2eqpr  6854  iunfidisj  6892  ctssdc  7059  cauappcvgprlemlol  7569  caucvgprlemlol  7592  caucvgprprlemlol  7620  elfzonelfzo  10138  qbtwnre  10165  nn0ltexp2  10595  hashun  10690  xrmaxltsup  11166  subcn2  11219  prodmodclem2  11485  divalglemex  11825  divalglemeuneg  11826  dvdslegcd  11863  lcmledvds  11962  modprmn0modprm0  12146  iscnp4  12688  cnrest2  12706  blssps  12897  blss  12898  bdbl  12973  metcnp3  12981  addcncntoplem  13021  cdivcncfap  13057