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  8144  poxp3  8151  pwfseqlem1  10724  pwfseqlem5  10729  icodiamlt  15585  issubc3  18004  pgpfac1lem5  20275  clsconn  23728  txlly  23935  txnlly  23936  itg2add  26060  ftc1a  26337  nosupprefixmo  28039  noinfprefixmo  28040  nosupbnd2  28055  noinfbnd2  28070  mulsprop  28498  bdayfinbndlem1  28835  f1otrg  29430  ax5seglem6  29494  axcontlem9  29532  axcontlem10  29533  elwspths2spth  30541  wwlksext2clwwlk  30630  locfinref  34455  erdszelem7  35931  cvmlift2lem10  36046  btwnouttr2  36757  btwnconn1lem13  36834  broutsideof2  36857  mpaaeu  44110  dfsalgen2  47295  fundcmpsurinjpreimafv  48434  grtrimap  48990  digexp  49663  line2xlem  49809