Theorem simprl1 1213

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

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

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 1084

This theorem is referenced by:  pwfseqlem1  10072  pwfseqlem5  10077  icodiamlt  14787  issubc3  17111  pgpfac1lem5  19193  clsconn  22030  txlly  22236  txnlly  22237  itg2add  24352  ftc1a  24626  f1otrg  26649  ax5seglem6  26712  axcontlem9  26750  axcontlem10  26751  elwspths2spth  27738  wwlksext2clwwlk  27828  locfinref  31098  erdszelem7  32437  cvmlift2lem10  32552  noprefixmo  33195  nosupbnd2  33209  btwnouttr2  33476  btwnconn1lem13  33553  broutsideof2  33576  mpaaeu  39741  dfsalgen2  42615  fundcmpsurinjpreimafv  43559  digexp  44658  line2xlem  44731