Theorem simprl1 1106

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

Assertion

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

Proof of Theorem simprl1

Step	Hyp	Ref	Expression
1		simpl1 1064	. 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:  pwfseqlem1  9480  pwfseqlem5  9485  icodiamlt  14174  issubc3  16509  pgpfac1lem5  18478  clsconn  21233  txlly  21439  txnlly  21440  itg2add  23526  ftc1a  23800  f1otrg  25751  ax5seglem6  25814  axcontlem9  25852  axcontlem10  25853  elwspths2spth  26862  locfinref  29908  erdszelem7  31179  cvmlift2lem10  31294  noprefixmo  31848  nosupbnd2  31862  btwnouttr2  32129  btwnconn1lem13  32206  broutsideof2  32229  mpaaeu  37720  dfsalgen2  40559  digexp  42401