Theorem simpll1 1032

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

Assertion

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

Proof of Theorem simpll1

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

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

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 976

This theorem is referenced by:  fidifsnen  6852  ordiso2  7016  ctssdc  7094  addlocpr  7502  xltadd1  9837  nn0ltexp2  10648  hashun  10744  fimaxq  10766  xrmaxltsup  11225  dvdslegcd  11923  lcmledvds  12028  divgcdcoprm0  12059  rpexp  12111  qexpz  12308  dfgrp3mlem  12801  iscnp4  13097  cnconst2  13112  blssps  13306  blss  13307  metcnp  13391  addcncntoplem  13430  cdivcncfap  13466  lgsfvalg  13785  lgsmod  13806  lgsdir  13815  lgsne0  13818