Theorem simprl1 1235

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  poxp2  8127  poxp3  8134  pwfseqlem1  10631  pwfseqlem5  10636  icodiamlt  15479  issubc3  17896  pgpfac1lem5  20142  clsconn  23548  txlly  23754  txnlly  23755  itg2add  25879  ftc1a  26157  nosupprefixmo  27822  noinfprefixmo  27823  nosupbnd2  27838  noinfbnd2  27853  mulsprop  28281  bdayfinbndlem1  28618  f1otrg  29129  ax5seglem6  29193  axcontlem9  29231  axcontlem10  29232  elwspths2spth  30228  wwlksext2clwwlk  30317  locfinref  34148  erdszelem7  35560  cvmlift2lem10  35675  btwnouttr2  36385  btwnconn1lem13  36462  broutsideof2  36485  mpaaeu  43739  dfsalgen2  46913  fundcmpsurinjpreimafv  48012  grtrimap  48568  digexp  49238  line2xlem  49384