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  8122  poxp3  8129  pwfseqlem1  10611  pwfseqlem5  10616  icodiamlt  15404  issubc3  17811  pgpfac1lem5  20011  clsconn  23317  txlly  23523  txnlly  23524  itg2add  25660  ftc1a  25944  nosupprefixmo  27612  noinfprefixmo  27613  nosupbnd2  27628  noinfbnd2  27643  mulsprop  28033  f1otrg  28798  ax5seglem6  28861  axcontlem9  28899  axcontlem10  28900  elwspths2spth  29897  wwlksext2clwwlk  29986  locfinref  33831  erdszelem7  35184  cvmlift2lem10  35299  btwnouttr2  36010  btwnconn1lem13  36087  broutsideof2  36110  mpaaeu  43139  dfsalgen2  46339  fundcmpsurinjpreimafv  47409  grtrimap  47947  digexp  48596  line2xlem  48742