Theorem simpll1 988

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

Assertion

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

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 952	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜑)
2	1	adantr 272	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

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

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

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

This theorem is referenced by:  fidifsnen  6693  ordiso2  6835  ctssdc  6912  addlocpr  7245  xltadd1  9500  hashun  10392  fimaxq  10414  xrmaxltsup  10866  dvdslegcd  11448  lcmledvds  11544  divgcdcoprm0  11575  rpexp  11624  iscnp4  12168  cnconst2  12183  blssps  12355  blss  12356  metcnp  12436  cdivcncfap  12499