Theorem mpbirand 706

Description: Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

Hypotheses

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

Assertion

Ref	Expression
mpbirand	⊢ (𝜑 → (𝜓 ↔ 𝜃))

Proof of Theorem mpbirand

Step	Hyp	Ref	Expression
1		mpbirand.2	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃)))
2		mpbirand.1	. . 3 ⊢ (𝜑 → 𝜒)
3	2	biantrurd 534	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 282	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  mpbiran2d  707  3anibar  1330  rmob2  3887  opbrop  5774  wemapso2lem  9547  uzin  12862  supxrre1  13309  ixxun  13340  uzsplit  13573  pfxsuffeqwrdeq  14648  ello12  15460  elo12  15471  fsumss  15671  fprodss  15892  ramval  16941  issect2  17701  lspsnel5  20606  cnprest  22793  cnprest2  22794  cnt0  22850  1stccn  22967  kgencn  23060  qtopcn  23218  fbflim  23480  isflf  23497  cnflf  23506  fclscf  23529  cnfcf  23546  elbl2ps  23895  elbl2  23896  metcn  24052  txmetcn  24057  iscvs  24643  lmclimf  24821  ovolfioo  24984  ovolficc  24985  ovoliun  25022  ismbl2  25044  mbfmulc2lem  25164  mbfmax  25166  mbfposr  25169  mbfaddlem  25177  mbfsup  25181  mbfi1fseqlem4  25236  itg2monolem1  25268  itg2cnlem1  25279  tgellng  27804  isleag  28098  ttgelitv  28140  isspthonpth  29006  clwlkclwwlkflem  29257  clwwlkwwlksb  29307  fvdifsupp  31907  lindflbs  32495  ismntoplly  33005  esum2dlem  33090  ntrclselnel1  42808  ntrneicls00  42840  vonvolmbl  45377  dfdfat2  45836  ipolubdm  47612  ipoglbdm  47615  functhinc  47665