Theorem simplrd 768

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  erinxp  8737  fpwwe2lem5  10580  fpwwe2lem6  10581  fpwwe2lem8  10583  lejoin2  18288  lemeet2  18302  dirdm  18503  dirref  18504  lmhmlmod2  20550  pi1cpbl  24444  pntlemr  26987  oppne2  27747  dfcgra2  27835  mgcf2  31919  mgccole2  31921  mgcmnt1  31922  mgcmnt2  31923  mgcf1olem1  31931  mgcf1olem2  31932  mgcf1o  31933  mtyf2  34232  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  fourierdlem48  44515  fourierdlem76  44543  fourierdlem80  44547  fourierdlem93  44560  fourierdlem94  44561  fourierdlem104  44571  fourierdlem113  44580  mea0  44815  meaiunlelem  44829  meaiuninclem  44841  omessle  44859  omedm  44860  carageniuncllem2  44883  hspmbllem3  44989