Theorem simprl3 1220

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)

Assertion

Ref	Expression
simprl3	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃)) → 𝜒)

Proof of Theorem simprl3

Step	Hyp	Ref	Expression
1		simp3 1138	. 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:  poxp3  8191  ttrcltr  9785  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  axcontlem10  29006  numclwwlk5  30420  locfinref  33787  btwnouttr2  35986  btwnconn1lem13  36063  midofsegid  36068  outsideofeq  36094  ivthALT  36301  mpaaeu  43107  dfsalgen2  46262  grtrimap  47797