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  8723  fpwwe2lem5  10535  fpwwe2lem6  10536  fpwwe2lem8  10538  lejoin2  18293  lemeet2  18307  dirdm  18510  dirref  18511  lmhmlmod2  20970  pi1cpbl  24974  pntlemr  27543  oppne2  28723  dfcgra2  28811  mgcf2  32979  mgccole2  32981  mgcmnt1  32982  mgcmnt2  32983  mgcf1olem1  32991  mgcf1olem2  32992  mgcf1o  32993  erlcl2  33237  erler  33241  mtyf2  35618  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  fourierdlem48  46279  fourierdlem76  46307  fourierdlem80  46311  fourierdlem93  46324  fourierdlem94  46325  fourierdlem104  46335  fourierdlem113  46344  mea0  46579  meaiunlelem  46593  meaiuninclem  46605  omessle  46623  omedm  46624  carageniuncllem2  46647  hspmbllem3  46753  sectpropdlem  49164  invpropdlem  49166  isopropdlem  49168  uprcl5  49320