Theorem simprl1 1237

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8162  poxp3  8169  pwfseqlem1  10746  pwfseqlem5  10751  icodiamlt  15610  issubc3  18029  pgpfac1lem5  20300  clsconn  23753  txlly  23960  txnlly  23961  itg2add  26085  ftc1a  26362  nosupprefixmo  28062  noinfprefixmo  28063  nosupbnd2  28078  noinfbnd2  28093  mulsprop  28521  bdayfinbndlem1  28858  f1otrg  29453  ax5seglem6  29517  axcontlem9  29555  axcontlem10  29556  elwspths2spth  30564  wwlksext2clwwlk  30653  locfinref  34519  erdszelem7  36048  cvmlift2lem10  36163  btwnouttr2  36879  btwnconn1lem13  36956  broutsideof2  36979  mpaaeu  44245  dfsalgen2  47444  fundcmpsurinjpreimafv  48583  grtrimap  49139  digexp  49812  line2xlem  49958