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  8187  poxp3  8194  pwfseqlem1  10770  pwfseqlem5  10775  icodiamlt  15634  issubc3  18053  pgpfac1lem5  20325  clsconn  23778  txlly  23985  txnlly  23986  itg2add  26110  ftc1a  26387  nosupprefixmo  28087  noinfprefixmo  28088  nosupbnd2  28103  noinfbnd2  28118  mulsprop  28546  bdayfinbndlem1  28883  f1otrg  29478  ax5seglem6  29542  axcontlem9  29580  axcontlem10  29581  elwspths2spth  30589  wwlksext2clwwlk  30678  locfinref  34543  erdszelem7  36129  cvmlift2lem10  36244  btwnouttr2  36965  btwnconn1lem13  37042  broutsideof2  37065  mpaaeu  44344  dfsalgen2  47556  fundcmpsurinjpreimafv  48695  grtrimap  49251  digexp  49924  line2xlem  50070