Theorem simprl1 1225

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  poxp2  8090  poxp3  8097  pwfseqlem1  10579  pwfseqlem5  10584  icodiamlt  15398  issubc3  17814  pgpfac1lem5  20054  clsconn  23420  txlly  23626  txnlly  23627  itg2add  25751  ftc1a  26029  nosupprefixmo  27689  noinfprefixmo  27690  nosupbnd2  27705  noinfbnd2  27720  mulsprop  28147  bdayfinbndlem1  28484  f1otrg  28964  ax5seglem6  29028  axcontlem9  29066  axcontlem10  29067  elwspths2spth  30063  wwlksext2clwwlk  30152  locfinref  34032  erdszelem7  35432  cvmlift2lem10  35547  btwnouttr2  36257  btwnconn1lem13  36334  broutsideof2  36357  mpaaeu  43602  dfsalgen2  46791  fundcmpsurinjpreimafv  47890  grtrimap  48446  digexp  49105  line2xlem  49251