Theorem simprl1 1217

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 1135	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antrl 725	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pwfseqlem1  10414  pwfseqlem5  10419  icodiamlt  15147  issubc3  17564  pgpfac1lem5  19682  clsconn  22581  txlly  22787  txnlly  22788  itg2add  24924  ftc1a  25201  f1otrg  27232  ax5seglem6  27302  axcontlem9  27340  axcontlem10  27341  elwspths2spth  28332  wwlksext2clwwlk  28421  locfinref  31791  erdszelem7  33159  cvmlift2lem10  33274  poxp2  33790  poxp3  33796  nosupprefixmo  33903  noinfprefixmo  33904  nosupbnd2  33919  noinfbnd2  33934  btwnouttr2  34324  btwnconn1lem13  34401  broutsideof2  34424  mpaaeu  40975  dfsalgen2  43880  fundcmpsurinjpreimafv  44860  digexp  45953  line2xlem  46099