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  8073  poxp3  8080  pwfseqlem1  10546  pwfseqlem5  10551  icodiamlt  15342  issubc3  17753  pgpfac1lem5  19991  clsconn  23343  txlly  23549  txnlly  23550  itg2add  25685  ftc1a  25969  nosupprefixmo  27637  noinfprefixmo  27638  nosupbnd2  27653  noinfbnd2  27668  mulsprop  28067  f1otrg  28847  ax5seglem6  28910  axcontlem9  28948  axcontlem10  28949  elwspths2spth  29943  wwlksext2clwwlk  30032  locfinref  33849  erdszelem7  35229  cvmlift2lem10  35344  btwnouttr2  36055  btwnconn1lem13  36132  broutsideof2  36155  mpaaeu  43182  dfsalgen2  46378  fundcmpsurinjpreimafv  47438  grtrimap  47978  digexp  48638  line2xlem  48784