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  10231  nn0ltexp2  11099  hashun  11197  fimaxq  11222  xrmaxltsup  11972  dvdslegcd  12689  lcmledvds  12796  divgcdcoprm0  12827  rpexp  12879  qexpz  13079  dfgrp3mlem  13857  rhmdvdsr  14424  rnglidlmcl  14758  iscnp4  15213  cnconst2  15228  blssps  15422  blss  15423  metcnp  15507  addcncntoplem  15556  cdivcncfap  15599  lgsfvalg  16008  lgsmod  16029  lgsdir  16038  lgsne0  16041  clwwlknonex2  16564  eulerpathum  16606