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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  poxp2  8148  poxp3  8155  pwfseqlem1  10661  pwfseqlem5  10666  icodiamlt  15515  issubc3  17931  pgpfac1lem5  20182  clsconn  23624  txlly  23830  txnlly  23831  itg2add  25955  ftc1a  26233  nosupprefixmo  27901  noinfprefixmo  27902  nosupbnd2  27917  noinfbnd2  27932  mulsprop  28360  bdayfinbndlem1  28697  f1otrg  29257  ax5seglem6  29321  axcontlem9  29359  axcontlem10  29360  elwspths2spth  30356  wwlksext2clwwlk  30445  locfinref  34262  erdszelem7  35710  cvmlift2lem10  35825  btwnouttr2  36535  btwnconn1lem13  36612  broutsideof2  36635  mpaaeu  43918  dfsalgen2  47096  fundcmpsurinjpreimafv  48198  grtrimap  48754  digexp  49428  line2xlem  49574