Theorem simpll1 1067

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

Assertion

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

Proof of Theorem simpll1

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

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

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 1011

This theorem is referenced by:  fidifsnen  7166  ordiso2  7369  ctssdc  7447  addlocpr  7897  xltadd1  10261  nn0ltexp2  11130  hashun  11228  fimaxq  11253  xrmaxltsup  12007  dvdslegcd  12724  lcmledvds  12831  divgcdcoprm0  12862  rpexp  12914  qexpz  13114  dfgrp3mlem  13886  gsumconstcmn  14149  rhmdvdsr  14465  rnglidlmcl  14800  iscnp4  15302  cnconst2  15317  blssps  15511  blss  15512  metcnp  15596  addcncntoplem  15645  cdivcncfap  15688  lgsfvalg  16107  lgsmod  16128  lgsdir  16137  lgsne0  16140  clwwlknonex2  16663  eulerpathum  16705