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  8093  poxp3  8100  pwfseqlem1  10581  pwfseqlem5  10586  icodiamlt  15400  issubc3  17816  pgpfac1lem5  20056  clsconn  23395  txlly  23601  txnlly  23602  itg2add  25726  ftc1a  26004  nosupprefixmo  27664  noinfprefixmo  27665  nosupbnd2  27680  noinfbnd2  27695  mulsprop  28122  bdayfinbndlem1  28459  f1otrg  28939  ax5seglem6  29003  axcontlem9  29041  axcontlem10  29042  elwspths2spth  30038  wwlksext2clwwlk  30127  locfinref  33985  erdszelem7  35379  cvmlift2lem10  35494  btwnouttr2  36204  btwnconn1lem13  36281  broutsideof2  36304  mpaaeu  43578  dfsalgen2  46769  fundcmpsurinjpreimafv  47868  grtrimap  48424  digexp  49083  line2xlem  49229