Theorem mpbiran2d 708

Description: Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)

Hypotheses

Ref	Expression
mpbiran2d.1	⊢ (𝜑 → 𝜃)
mpbiran2d.2	⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))

Assertion

Ref	Expression
mpbiran2d	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Proof of Theorem mpbiran2d

Step	Hyp	Ref	Expression
1		mpbiran2d.1	. 2 ⊢ (𝜑 → 𝜃)
2		mpbiran2d.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
3	2	biancomd 463	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜃 ∧ 𝜒)))
4	1, 3	mpbirand 707	1 ⊢ (𝜑 → (𝜓 ↔ 𝜒))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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:  opelidres  5950  funsnfsupp  9295  discld  23033  cncfcdm  24847  itgfsum  25784  dchreq  27225  lgsneg  27288  lgsquadlem2  27348  z12bdaylem1  28466  dfconngr1  30263  cover2  37916  iscnrm3rlem6  49190  0funcglem  49328  0funcg2  49329  thincmon  49678  thincepi  49679