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  8147  poxp3  8154  pwfseqlem1  10677  pwfseqlem5  10682  icodiamlt  15459  issubc3  17867  pgpfac1lem5  20067  clsconn  23373  txlly  23579  txnlly  23580  itg2add  25717  ftc1a  26001  nosupprefixmo  27669  noinfprefixmo  27670  nosupbnd2  27685  noinfbnd2  27700  mulsprop  28090  f1otrg  28855  ax5seglem6  28918  axcontlem9  28956  axcontlem10  28957  elwspths2spth  29954  wwlksext2clwwlk  30043  locfinref  33877  erdszelem7  35224  cvmlift2lem10  35339  btwnouttr2  36045  btwnconn1lem13  36122  broutsideof2  36145  mpaaeu  43141  dfsalgen2  46337  fundcmpsurinjpreimafv  47389  grtrimap  47927  digexp  48554  line2xlem  48700