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  8125  poxp3  8132  pwfseqlem1  10618  pwfseqlem5  10623  icodiamlt  15411  issubc3  17818  pgpfac1lem5  20018  clsconn  23324  txlly  23530  txnlly  23531  itg2add  25667  ftc1a  25951  nosupprefixmo  27619  noinfprefixmo  27620  nosupbnd2  27635  noinfbnd2  27650  mulsprop  28040  f1otrg  28805  ax5seglem6  28868  axcontlem9  28906  axcontlem10  28907  elwspths2spth  29904  wwlksext2clwwlk  29993  locfinref  33838  erdszelem7  35191  cvmlift2lem10  35306  btwnouttr2  36017  btwnconn1lem13  36094  broutsideof2  36117  mpaaeu  43146  dfsalgen2  46346  fundcmpsurinjpreimafv  47413  grtrimap  47951  digexp  48600  line2xlem  48746