Theorem simpll1 1063

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

Assertion

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

Proof of Theorem simpll1

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

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

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 1007

This theorem is referenced by:  fidifsnen  7138  ordiso2  7339  ctssdc  7417  addlocpr  7867  xltadd1  10228  nn0ltexp2  11096  hashun  11194  fimaxq  11219  xrmaxltsup  11968  dvdslegcd  12685  lcmledvds  12792  divgcdcoprm0  12823  rpexp  12875  qexpz  13075  dfgrp3mlem  13895  rhmdvdsr  14405  rnglidlmcl  14740  iscnp4  15195  cnconst2  15210  blssps  15404  blss  15405  metcnp  15489  addcncntoplem  15538  cdivcncfap  15581  lgsfvalg  15990  lgsmod  16011  lgsdir  16020  lgsne0  16023  clwwlknonex2  16546  eulerpathum  16588