Theorem simprl1 1231

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 1148	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrl 738	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  poxp2  8118  poxp3  8125  pwfseqlem1  10613  pwfseqlem5  10618  icodiamlt  15448  issubc3  17865  pgpfac1lem5  20104  clsconn  23470  txlly  23676  txnlly  23677  itg2add  25801  ftc1a  26079  nosupprefixmo  27741  noinfprefixmo  27742  nosupbnd2  27757  noinfbnd2  27772  mulsprop  28200  bdayfinbndlem1  28537  f1otrg  29017  ax5seglem6  29081  axcontlem9  29119  axcontlem10  29120  elwspths2spth  30116  wwlksext2clwwlk  30205  locfinref  34099  erdszelem7  35511  cvmlift2lem10  35626  btwnouttr2  36336  btwnconn1lem13  36413  broutsideof2  36436  mpaaeu  43691  dfsalgen2  46879  fundcmpsurinjpreimafv  47978  grtrimap  48534  digexp  49193  line2xlem  49339