Theorem simprl1 1220

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

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

Proof of Theorem simprl1

Step	Hyp	Ref	Expression
1		simp1 1137	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrl 729	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  poxp2  8086  poxp3  8093  pwfseqlem1  10572  pwfseqlem5  10577  icodiamlt  15391  issubc3  17807  pgpfac1lem5  20047  clsconn  23405  txlly  23611  txnlly  23612  itg2add  25736  ftc1a  26014  nosupprefixmo  27678  noinfprefixmo  27679  nosupbnd2  27694  noinfbnd2  27709  mulsprop  28136  bdayfinbndlem1  28473  f1otrg  28953  ax5seglem6  29017  axcontlem9  29055  axcontlem10  29056  elwspths2spth  30053  wwlksext2clwwlk  30142  locfinref  34001  erdszelem7  35395  cvmlift2lem10  35510  btwnouttr2  36220  btwnconn1lem13  36297  broutsideof2  36320  mpaaeu  43596  dfsalgen2  46787  fundcmpsurinjpreimafv  47880  grtrimap  48436  digexp  49095  line2xlem  49241