Theorem simpll1 1031

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

Assertion

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

Proof of Theorem simpll1

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

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

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 975

This theorem is referenced by:  fidifsnen  6846  ordiso2  7010  ctssdc  7088  addlocpr  7491  xltadd1  9826  nn0ltexp2  10637  hashun  10733  fimaxq  10755  xrmaxltsup  11214  dvdslegcd  11912  lcmledvds  12017  divgcdcoprm0  12048  rpexp  12100  qexpz  12297  iscnp4  12977  cnconst2  12992  blssps  13186  blss  13187  metcnp  13271  addcncntoplem  13310  cdivcncfap  13346  lgsfvalg  13665  lgsmod  13686  lgsdir  13695  lgsne0  13698