Theorem simprl1 1282

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

Syntax hints:   → wi 4   ∧ wa 385   ∧ w3a 1108

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 199  df-an 386  df-3an 1110

This theorem is referenced by:  pwfseqlem1  9768  pwfseqlem5  9773  icodiamlt  14515  issubc3  16823  pgpfac1lem5  18794  clsconn  21562  txlly  21768  txnlly  21769  itg2add  23867  ftc1a  24141  f1otrg  26108  ax5seglem6  26171  axcontlem9  26209  axcontlem10  26210  elwspths2spth  27258  wwlksext2clwwlk  27373  locfinref  30424  erdszelem7  31696  cvmlift2lem10  31811  noprefixmo  32361  nosupbnd2  32375  btwnouttr2  32642  btwnconn1lem13  32719  broutsideof2  32742  mpaaeu  38505  dfsalgen2  41302  digexp  43200