Theorem simprl1 1215

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  pwfseqlem1  10069  pwfseqlem5  10074  icodiamlt  14787  issubc3  17111  pgpfac1lem5  19194  clsconn  22035  txlly  22241  txnlly  22242  itg2add  24363  ftc1a  24640  f1otrg  26665  ax5seglem6  26728  axcontlem9  26766  axcontlem10  26767  elwspths2spth  27753  wwlksext2clwwlk  27842  locfinref  31194  erdszelem7  32557  cvmlift2lem10  32672  noprefixmo  33315  nosupbnd2  33329  btwnouttr2  33596  btwnconn1lem13  33673  broutsideof2  33696  mpaaeu  40094  dfsalgen2  42981  fundcmpsurinjpreimafv  43925  digexp  45021  line2xlem  45167