Theorem simplrd 769

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 494	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 495	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  erinxp  8805  fpwwe2lem5  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  lejoin2  18395  lemeet2  18409  dirdm  18610  dirref  18611  lmhmlmod2  20990  pi1cpbl  24995  pntlemr  27565  oppne2  28721  dfcgra2  28809  mgcf2  32969  mgccole2  32971  mgcmnt1  32972  mgcmnt2  32973  mgcf1olem1  32981  mgcf1olem2  32982  mgcf1o  32983  erlcl2  33256  erler  33260  mtyf2  35573  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  fourierdlem48  46183  fourierdlem76  46211  fourierdlem80  46215  fourierdlem93  46228  fourierdlem94  46229  fourierdlem104  46239  fourierdlem113  46248  mea0  46483  meaiunlelem  46497  meaiuninclem  46509  omessle  46527  omedm  46528  carageniuncllem2  46551  hspmbllem3  46657  sectpropdlem  49003  invpropdlem  49005  isopropdlem  49007  uprcl5  49126