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  7124  ordiso2  7325  ctssdc  7403  addlocpr  7850  xltadd1  10208  nn0ltexp2  11070  hashun  11167  fimaxq  11190  xrmaxltsup  11939  dvdslegcd  12656  lcmledvds  12763  divgcdcoprm0  12794  rpexp  12846  qexpz  13046  dfgrp3mlem  13803  rhmdvdsr  14312  rnglidlmcl  14620  iscnp4  15075  cnconst2  15090  blssps  15284  blss  15285  metcnp  15369  addcncntoplem  15418  cdivcncfap  15461  lgsfvalg  15870  lgsmod  15891  lgsdir  15900  lgsne0  15903  clwwlknonex2  16426  eulerpathum  16468