Theorem mpbirand 707

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 532	. 2 ⊢ (𝜑 → (𝜃 ↔ (𝜒 ∧ 𝜃)))
4	1, 3	bitr4d 282	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:  mpbiran2d  708  3anibar  1330  rmob2  3842  opbrop  5722  fvdifsupp  8113  wemapso2lem  9457  uzin  12787  supxrre1  13245  ixxun  13277  uzsplit  13512  pfxsuffeqwrdeq  14621  ello12  15439  elo12  15450  fsumss  15648  fprodss  15871  ramval  16936  issect2  17678  ellspsn5b  20946  cnprest  23233  cnprest2  23234  cnt0  23290  1stccn  23407  kgencn  23500  qtopcn  23658  fbflim  23920  isflf  23937  cnflf  23946  fclscf  23969  cnfcf  23986  elbl2ps  24333  elbl2  24334  metcn  24487  txmetcn  24492  iscvs  25083  lmclimf  25260  ovolfioo  25424  ovolficc  25425  ovoliun  25462  ismbl2  25484  mbfmulc2lem  25604  mbfmax  25606  mbfposr  25609  mbfaddlem  25617  mbfsup  25621  mbfi1fseqlem4  25675  itg2monolem1  25707  itg2cnlem1  25718  tgellng  28625  isleag  28919  ttgelitv  28955  isspthonpth  29822  clwlkclwwlkflem  30079  clwwlkwwlksb  30129  isfxp  33250  lindflbs  33460  ply1degleel  33676  algextdeglem7  33880  ismntoplly  34182  esum2dlem  34249  ntrclselnel1  44294  ntrneicls00  44326  vonvolmbl  46901  dfdfat2  47370  ipolubdm  49228  ipoglbdm  49231  isup  49421  functhinc  49689