Theorem simprl1 1237

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  poxp2  8140  poxp3  8147  pwfseqlem1  10644  pwfseqlem5  10649  icodiamlt  15491  issubc3  17907  pgpfac1lem5  20152  clsconn  23568  txlly  23774  txnlly  23775  itg2add  25899  ftc1a  26177  nosupprefixmo  27842  noinfprefixmo  27843  nosupbnd2  27858  noinfbnd2  27873  mulsprop  28301  bdayfinbndlem1  28638  f1otrg  29198  ax5seglem6  29262  axcontlem9  29300  axcontlem10  29301  elwspths2spth  30297  wwlksext2clwwlk  30386  locfinref  34209  erdszelem7  35667  cvmlift2lem10  35782  btwnouttr2  36492  btwnconn1lem13  36569  broutsideof2  36592  mpaaeu  43857  dfsalgen2  47035  fundcmpsurinjpreimafv  48134  grtrimap  48690  digexp  49364  line2xlem  49510