Theorem mpbiran2d 709

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 708	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  5958  funsnfsupp  9307  discld  23045  cncfcdm  24859  itgfsum  25796  dchreq  27237  lgsneg  27300  lgsquadlem2  27360  z12bdaylem1  28478  dfconngr1  30275  cover2  37963  iscnrm3rlem6  49301  0funcglem  49439  0funcg2  49440  thincmon  49789  thincepi  49790