Theorem simplld 764

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

Hypothesis

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

Assertion

Ref	Expression
simplld	⊢ (𝜑 → 𝜓)

Proof of Theorem simplld

Step	Hyp	Ref	Expression
1		simplld.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ∧ 𝜃))
2	1	simpld 494	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 494	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 206  df-an 396

This theorem is referenced by:  erinxp  8538  lejoin1  18017  lemeet1  18031  reldir  18232  gexdvdsi  19103  lmhmlmod1  20210  pi1cpbl  24113  oppne1  27006  trgcopyeulem  27070  dfcgra2  27095  subupgr  27557  3trlond  28438  3pthond  28440  3spthond  28442  grpolid  28779  mgcf1  31168  mgccole1  31170  mgcmnt1  31172  mgcmnt2  31173  mgcf1olem1  31181  mgcf1olem2  31182  mgcf1o  31183  mfsdisj  33412  linethru  34382  rngoablo  35993  fourierdlem37  43575  fourierdlem48  43585  fourierdlem93  43630  fourierdlem94  43631  fourierdlem104  43641  fourierdlem112  43649  fourierdlem113  43650  dmmeasal  43880  meaf  43881  meaiuninclem  43908  omef  43924  ome0  43925  omedm  43927  hspmbllem3  44056