Theorem simprl1 1219

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

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

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 1088

This theorem is referenced by:  poxp2  8083  poxp3  8090  pwfseqlem1  10571  pwfseqlem5  10576  icodiamlt  15363  issubc3  17774  pgpfac1lem5  19978  clsconn  23333  txlly  23539  txnlly  23540  itg2add  25676  ftc1a  25960  nosupprefixmo  27628  noinfprefixmo  27629  nosupbnd2  27644  noinfbnd2  27659  mulsprop  28056  f1otrg  28834  ax5seglem6  28897  axcontlem9  28935  axcontlem10  28936  elwspths2spth  29930  wwlksext2clwwlk  30019  locfinref  33807  erdszelem7  35169  cvmlift2lem10  35284  btwnouttr2  35995  btwnconn1lem13  36072  broutsideof2  36095  mpaaeu  43123  dfsalgen2  46323  fundcmpsurinjpreimafv  47393  grtrimap  47933  digexp  48593  line2xlem  48739