Theorem simpll1 1038

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

Assertion

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

Proof of Theorem simpll1

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

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

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 982

This theorem is referenced by:  fidifsnen  6931  ordiso2  7101  ctssdc  7179  addlocpr  7603  xltadd1  9951  nn0ltexp2  10801  hashun  10897  fimaxq  10919  xrmaxltsup  11423  dvdslegcd  12131  lcmledvds  12238  divgcdcoprm0  12269  rpexp  12321  qexpz  12521  dfgrp3mlem  13230  rhmdvdsr  13731  rnglidlmcl  14036  iscnp4  14454  cnconst2  14469  blssps  14663  blss  14664  metcnp  14748  addcncntoplem  14797  cdivcncfap  14840  lgsfvalg  15246  lgsmod  15267  lgsdir  15276  lgsne0  15279