Theorem simplrd 770

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  8731  fpwwe2lem5  10549  fpwwe2lem6  10550  fpwwe2lem8  10552  lejoin2  18340  lemeet2  18354  dirdm  18557  dirref  18558  lmhmlmod2  21019  pi1cpbl  25021  pntlemr  27579  oppne2  28824  dfcgra2  28912  mgcf2  33064  mgccole2  33066  mgcmnt1  33067  mgcmnt2  33068  mgcf1olem1  33076  mgcf1olem2  33077  mgcf1o  33078  erlcl2  33337  erler  33341  mtyf2  35749  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  fourierdlem48  46600  fourierdlem76  46628  fourierdlem80  46632  fourierdlem93  46645  fourierdlem94  46646  fourierdlem104  46656  fourierdlem113  46665  mea0  46900  meaiunlelem  46914  meaiuninclem  46926  omessle  46944  omedm  46945  carageniuncllem2  46968  hspmbllem3  47074  sectpropdlem  49523  invpropdlem  49525  isopropdlem  49527  uprcl5  49679