Theorem mpbirand 705

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 535	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 284	1 ⊢ (𝜑 → (𝜓 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  mpbiran2d  706  3anibar  1325  rmob2  3876  opbrop  5648  wemapso2lem  9016  uzin  12279  supxrre1  12724  ixxun  12755  uzsplit  12980  pfxsuffeqwrdeq  14060  ello12  14873  elo12  14884  fsumss  15082  fprodss  15302  ramval  16344  issect2  17024  lspsnel5  19767  cnprest  21897  cnprest2  21898  cnt0  21954  1stccn  22071  kgencn  22164  qtopcn  22322  fbflim  22584  isflf  22601  cnflf  22610  fclscf  22633  cnfcf  22650  elbl2ps  22999  elbl2  23000  metcn  23153  txmetcn  23158  iscvs  23731  lmclimf  23907  ovolfioo  24068  ovolficc  24069  ovoliun  24106  ismbl2  24128  mbfmulc2lem  24248  mbfmax  24250  mbfposr  24253  mbfaddlem  24261  mbfsup  24265  mbfi1fseqlem4  24319  itg2monolem1  24351  itg2cnlem1  24362  tgellng  26339  isleag  26633  ttgelitv  26669  isspthonpth  27530  clwlkclwwlkflem  27782  clwwlkwwlksb  27833  fvdifsupp  30427  lindflbs  30940  ismntoplly  31266  esum2dlem  31351  ntrclselnel1  40427  ntrneicls00  40459  vonvolmbl  42963  dfdfat2  43347