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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  fidifsnen  7177  ordiso2  7382  ctssdc  7460  addlocpr  7910  xltadd1  10296  nn0ltexp2  11170  hashun  11268  fimaxq  11293  xrmaxltsup  12050  dvdslegcd  12767  lcmledvds  12874  divgcdcoprm0  12905  rpexp  12958  qexpz  13161  dfgrp3mlem  13963  gsumconstcmn  14267  rhmdvdsr  14592  rnglidlmcl  14927  iscnp4  15456  cnconst2  15471  blssps  15665  blss  15666  metcnp  15750  addcncntoplem  15799  cdivcncfap  15842  lgsfvalg  16341  lgsmod  16362  lgsdir  16371  lgsne0  16374  clwwlknonex2  16897  eulerpathum  16939