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  7172  ordiso2  7375  ctssdc  7453  addlocpr  7903  xltadd1  10280  nn0ltexp2  11149  hashun  11247  fimaxq  11272  xrmaxltsup  12026  dvdslegcd  12743  lcmledvds  12850  divgcdcoprm0  12881  rpexp  12933  qexpz  13133  dfgrp3mlem  13905  gsumconstcmn  14168  rhmdvdsr  14484  rnglidlmcl  14819  iscnp4  15321  cnconst2  15336  blssps  15530  blss  15531  metcnp  15615  addcncntoplem  15664  cdivcncfap  15707  lgsfvalg  16136  lgsmod  16157  lgsdir  16166  lgsne0  16169  clwwlknonex2  16692  eulerpathum  16734