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  8085  poxp3  8092  pwfseqlem1  10569  pwfseqlem5  10574  icodiamlt  15361  issubc3  17773  pgpfac1lem5  20010  clsconn  23374  txlly  23580  txnlly  23581  itg2add  25716  ftc1a  26000  nosupprefixmo  27668  noinfprefixmo  27669  nosupbnd2  27684  noinfbnd2  27699  mulsprop  28126  bdayfinbndlem1  28463  f1otrg  28943  ax5seglem6  29007  axcontlem9  29045  axcontlem10  29046  elwspths2spth  30043  wwlksext2clwwlk  30132  locfinref  33998  erdszelem7  35391  cvmlift2lem10  35506  btwnouttr2  36216  btwnconn1lem13  36293  broutsideof2  36316  mpaaeu  43388  dfsalgen2  46581  fundcmpsurinjpreimafv  47650  grtrimap  48190  digexp  48849  line2xlem  48995