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  3875  opbrop  5642  wemapso2lem  9010  uzin  12272  supxrre1  12717  ixxun  12748  uzsplit  12973  pfxsuffeqwrdeq  14054  ello12  14867  elo12  14878  fsumss  15076  fprodss  15296  ramval  16338  issect2  17018  lspsnel5  19761  cnprest  21891  cnprest2  21892  cnt0  21948  1stccn  22065  kgencn  22158  qtopcn  22316  fbflim  22578  isflf  22595  cnflf  22604  fclscf  22627  cnfcf  22644  elbl2ps  22993  elbl2  22994  metcn  23147  txmetcn  23152  iscvs  23725  lmclimf  23901  ovolfioo  24062  ovolficc  24063  ovoliun  24100  ismbl2  24122  mbfmulc2lem  24242  mbfmax  24244  mbfposr  24247  mbfaddlem  24255  mbfsup  24259  mbfi1fseqlem4  24313  itg2monolem1  24345  itg2cnlem1  24356  tgellng  26333  isleag  26627  ttgelitv  26663  isspthonpth  27524  clwlkclwwlkflem  27776  clwwlkwwlksb  27827  fvdifsupp  30421  lindflbs  30935  ismntoplly  31261  esum2dlem  31346  ntrclselnel1  40400  ntrneicls00  40432  vonvolmbl  42937  dfdfat2  43321