Theorem simprl3 1108

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

Assertion

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

Proof of Theorem simprl3

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  pwfseqlem5  9485  icodiamlt  14174  issubc3  16509  pgpfac1lem5  18478  clsconn  21233  txlly  21439  txnlly  21440  itg2add  23526  ftc1a  23800  f1otrg  25751  ax5seglem6  25814  axcontlem10  25853  numclwwlk5  27246  locfinref  29908  noprefixmo  31848  nosupbnd2  31862  btwnouttr2  32129  btwnconn1lem13  32206  midofsegid  32211  outsideofeq  32237  ivthALT  32330  mpaaeu  37720  dfsalgen2  40559