Theorem simprl1 1220

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

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

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 1089

This theorem is referenced by:  poxp2  8084  poxp3  8091  pwfseqlem1  10570  pwfseqlem5  10575  icodiamlt  15389  issubc3  17805  pgpfac1lem5  20045  clsconn  23404  txlly  23610  txnlly  23611  itg2add  25735  ftc1a  26016  nosupprefixmo  27683  noinfprefixmo  27684  nosupbnd2  27699  noinfbnd2  27714  mulsprop  28141  bdayfinbndlem1  28478  f1otrg  28958  ax5seglem6  29022  axcontlem9  29060  axcontlem10  29061  elwspths2spth  30058  wwlksext2clwwlk  30147  locfinref  34006  erdszelem7  35400  cvmlift2lem10  35515  btwnouttr2  36225  btwnconn1lem13  36302  broutsideof2  36325  mpaaeu  43593  dfsalgen2  46784  fundcmpsurinjpreimafv  47865  grtrimap  48421  digexp  49080  line2xlem  49226