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  3867  opbrop  5752  fvdifsupp  8170  wemapso2lem  9566  uzin  12892  supxrre1  13346  ixxun  13378  uzsplit  13613  pfxsuffeqwrdeq  14716  ello12  15532  elo12  15543  fsumss  15741  fprodss  15964  ramval  17028  issect2  17767  ellspsn5b  20952  cnprest  23227  cnprest2  23228  cnt0  23284  1stccn  23401  kgencn  23494  qtopcn  23652  fbflim  23914  isflf  23931  cnflf  23940  fclscf  23963  cnfcf  23980  elbl2ps  24328  elbl2  24329  metcn  24482  txmetcn  24487  iscvs  25078  lmclimf  25256  ovolfioo  25420  ovolficc  25421  ovoliun  25458  ismbl2  25480  mbfmulc2lem  25600  mbfmax  25602  mbfposr  25605  mbfaddlem  25613  mbfsup  25617  mbfi1fseqlem4  25671  itg2monolem1  25703  itg2cnlem1  25714  tgellng  28532  isleag  28826  ttgelitv  28862  isspthonpth  29731  clwlkclwwlkflem  29985  clwwlkwwlksb  30035  lindflbs  33394  ply1degleel  33605  algextdeglem7  33757  ismntoplly  34056  esum2dlem  34123  ntrclselnel1  44081  ntrneicls00  44113  vonvolmbl  46690  dfdfat2  47157  ipolubdm  48961  ipoglbdm  48964  isup  49115  functhinc  49334