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  8145  poxp3  8152  pwfseqlem1  10671  pwfseqlem5  10676  icodiamlt  15529  issubc3  17944  pgpfac1lem5  20214  clsconn  23661  txlly  23868  txnlly  23869  itg2add  25993  ftc1a  26271  nosupprefixmo  27944  noinfprefixmo  27945  nosupbnd2  27960  noinfbnd2  27975  mulsprop  28403  bdayfinbndlem1  28740  f1otrg  29335  ax5seglem6  29399  axcontlem9  29437  axcontlem10  29438  elwspths2spth  30446  wwlksext2clwwlk  30535  locfinref  34359  erdszelem7  35784  cvmlift2lem10  35899  btwnouttr2  36610  btwnconn1lem13  36687  broutsideof2  36710  mpaaeu  43999  dfsalgen2  47177  fundcmpsurinjpreimafv  48316  grtrimap  48872  digexp  49545  line2xlem  49691