Theorem simprl1 1218

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  poxp2  8184  poxp3  8191  pwfseqlem1  10727  pwfseqlem5  10732  icodiamlt  15484  issubc3  17913  pgpfac1lem5  20123  clsconn  23459  txlly  23665  txnlly  23666  itg2add  25814  ftc1a  26098  nosupprefixmo  27763  noinfprefixmo  27764  nosupbnd2  27779  noinfbnd2  27794  mulsprop  28174  f1otrg  28897  ax5seglem6  28967  axcontlem9  29005  axcontlem10  29006  elwspths2spth  30000  wwlksext2clwwlk  30089  locfinref  33787  erdszelem7  35165  cvmlift2lem10  35280  btwnouttr2  35986  btwnconn1lem13  36063  broutsideof2  36086  mpaaeu  43107  dfsalgen2  46262  fundcmpsurinjpreimafv  47282  grtrimap  47797  digexp  48341  line2xlem  48487