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  7039  fidifsnen  7040  en2eqpr  7077  iunfidisj  7121  ctssdc  7288  cauappcvgprlemlol  7842  caucvgprlemlol  7865  caucvgprprlemlol  7893  elfzonelfzo  10444  qbtwnre  10484  nn0ltexp2  10939  hashun  11035  swrdclg  11190  xrmaxltsup  11777  subcn2  11830  prodmodclem2  12096  divalglemex  12441  divalglemeuneg  12442  dvdslegcd  12493  lcmledvds  12600  modprmn0modprm0  12787  qexpz  12883  rnglidlmcl  14452  iscnp4  14900  cnrest2  14918  blssps  15109  blss  15110  bdbl  15185  metcnp3  15193  addcncntoplem  15243  cdivcncfap  15286  lgsfcl2  15693  lgsdir  15722  lgsne0  15725