Theorem simprl1 1216

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  pwfseqlem1  10345  pwfseqlem5  10350  icodiamlt  15075  issubc3  17480  pgpfac1lem5  19597  clsconn  22489  txlly  22695  txnlly  22696  itg2add  24829  ftc1a  25106  f1otrg  27136  ax5seglem6  27205  axcontlem9  27243  axcontlem10  27244  elwspths2spth  28233  wwlksext2clwwlk  28322  locfinref  31693  erdszelem7  33059  cvmlift2lem10  33174  poxp2  33717  poxp3  33723  nosupprefixmo  33830  noinfprefixmo  33831  nosupbnd2  33846  noinfbnd2  33861  btwnouttr2  34251  btwnconn1lem13  34328  broutsideof2  34351  mpaaeu  40891  dfsalgen2  43770  fundcmpsurinjpreimafv  44748  digexp  45841  line2xlem  45987