Theorem simpll1 1060

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

Assertion

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

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 1024	. 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:  fidifsnen  7040  ordiso2  7210  ctssdc  7288  addlocpr  7731  xltadd1  10080  nn0ltexp2  10939  hashun  11035  fimaxq  11057  xrmaxltsup  11777  dvdslegcd  12493  lcmledvds  12600  divgcdcoprm0  12631  rpexp  12683  qexpz  12883  dfgrp3mlem  13639  rhmdvdsr  14147  rnglidlmcl  14452  iscnp4  14900  cnconst2  14915  blssps  15109  blss  15110  metcnp  15194  addcncntoplem  15243  cdivcncfap  15286  lgsfvalg  15692  lgsmod  15713  lgsdir  15722  lgsne0  15725