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  8079  poxp3  8086  pwfseqlem1  10556  pwfseqlem5  10561  icodiamlt  15347  issubc3  17758  pgpfac1lem5  19995  clsconn  23346  txlly  23552  txnlly  23553  itg2add  25688  ftc1a  25972  nosupprefixmo  27640  noinfprefixmo  27641  nosupbnd2  27656  noinfbnd2  27671  mulsprop  28070  f1otrg  28850  ax5seglem6  28914  axcontlem9  28952  axcontlem10  28953  elwspths2spth  29950  wwlksext2clwwlk  30039  locfinref  33875  erdszelem7  35262  cvmlift2lem10  35377  btwnouttr2  36087  btwnconn1lem13  36164  broutsideof2  36187  mpaaeu  43267  dfsalgen2  46463  fundcmpsurinjpreimafv  47532  grtrimap  48072  digexp  48732  line2xlem  48878