Theorem simpll3 1062

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

Assertion

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

Proof of Theorem simpll3

Step	Hyp	Ref	Expression
1		simpl3 1026	. 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  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  frirrg  4442  fidceq  7044  fidifsnen  7045  en2eqpr  7085  iunfidisj  7129  ordiso2  7218  addlocpr  7739  aptiprlemu  7843  xltadd1  10089  xlesubadd  10096  icoshftf1o  10204  fztri3or  10252  elfzonelfzo  10453  exp3val  10780  nn0ltexp2  10948  hashun  11044  swrdclg  11203  subcn2  11843  divalglemeuneg  12455  dvdslegcd  12506  lcmledvds  12613  rpdvds  12642  cncongr2  12647  qexpz  12896  iuncld  14810  iscnp4  14913  cnpnei  14914  cnconst2  14928  cnpdis  14937  txcn  14970  blssps  15122  blss  15123  metcnp3  15206  metcnp  15207  lgsfcl2  15706  lgsdir  15735  lgsne0  15738