Theorem simprl3 1101

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

Assertion

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

Proof of Theorem simprl3

Step	Hyp	Ref	Expression
1		simpl3 1059	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜒)
2	1	adantl 481	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  pwfseqlem5  9364  icodiamlt  14022  issubc3  16332  pgpfac1lem5  18301  clscon  21043  txlly  21249  txnlly  21250  itg2add  23332  ftc1a  23604  f1otrg  25551  ax5seglem6  25614  axcontlem10  25653  numclwwlk5  26639  locfinref  29236  btwnouttr2  31299  btwnconn1lem13  31376  midofsegid  31381  outsideofeq  31407  ivthALT  31500  mpaaeu  36739  dfsalgen2  39235  av-numclwwlk5  41542