Theorem simprl1 1214

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pwfseqlem1  10079  pwfseqlem5  10084  icodiamlt  14794  issubc3  17118  pgpfac1lem5  19200  clsconn  22037  txlly  22243  txnlly  22244  itg2add  24359  ftc1a  24633  f1otrg  26656  ax5seglem6  26719  axcontlem9  26757  axcontlem10  26758  elwspths2spth  27745  wwlksext2clwwlk  27835  locfinref  31105  erdszelem7  32444  cvmlift2lem10  32559  noprefixmo  33202  nosupbnd2  33216  btwnouttr2  33483  btwnconn1lem13  33560  broutsideof2  33583  mpaaeu  39748  dfsalgen2  42623  fundcmpsurinjpreimafv  43567  digexp  44666  line2xlem  44739