Theorem simplrd 782

Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypothesis

Ref	Expression
simplrd.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))

Assertion

Ref	Expression
simplrd	⊢ (𝜑 → 𝜒)

Proof of Theorem simplrd

Step	Hyp	Ref	Expression
1		simplrd.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
2	1	simpld 500	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 501	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem is used by:  erinxp  8816  fpwwe2lem5  10724  fpwwe2lem6  10725  fpwwe2lem8  10727  lejoin2  18563  lemeet2  18577  dirdm  18780  dirref  18781  lmhmlmod2  21313  pi1cpbl  25371  pntlemr  27935  hlgrcl2  29073  oppne2  29224  dfcgra2  29344  cgraer  29383  angmgmlem  29401  prlngrcl2  29427  mgcf2  33597  mgccole2  33599  mgcmnt1  33600  mgcmnt2  33601  mgcf1olem1  33609  mgcf1olem2  33610  mgcf1o  33611  erlcl2  33869  erler  33873  mtyf2  36403  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  fourierdlem48  47258  fourierdlem76  47286  fourierdlem80  47290  fourierdlem93  47303  fourierdlem94  47304  fourierdlem104  47314  fourierdlem113  47323  mea0  47558  meaiunlelem  47572  meaiuninclem  47584  omessle  47602  omedm  47603  carageniuncllem2  47626  hspmbllem3  47732  sectpropdlem  50244  invpropdlem  50246  isopropdlem  50248  uprcl5  50402