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  8095  poxp3  8102  pwfseqlem1  10581  pwfseqlem5  10586  icodiamlt  15373  issubc3  17785  pgpfac1lem5  20022  clsconn  23386  txlly  23592  txnlly  23593  itg2add  25728  ftc1a  26012  nosupprefixmo  27680  noinfprefixmo  27681  nosupbnd2  27696  noinfbnd2  27711  mulsprop  28138  bdayfinbndlem1  28475  f1otrg  28955  ax5seglem6  29019  axcontlem9  29057  axcontlem10  29058  elwspths2spth  30055  wwlksext2clwwlk  30144  locfinref  34018  erdszelem7  35410  cvmlift2lem10  35525  btwnouttr2  36235  btwnconn1lem13  36312  broutsideof2  36335  mpaaeu  43501  dfsalgen2  46693  fundcmpsurinjpreimafv  47762  grtrimap  48302  digexp  48961  line2xlem  49107